diff --git a/CommonLogic/Analysis.hs b/CommonLogic/Analysis.hs
index fd23b6fe8f..9dcc82eb63 100644
--- a/CommonLogic/Analysis.hs
+++ b/CommonLogic/Analysis.hs
@@ -20,6 +20,7 @@ module CommonLogic.Analysis
     , inducedFromMorphism
     , inducedFromToMorphism
     , signColimit
+    , convertBasicTheory
     )
     where
 
@@ -397,3 +398,9 @@ signColimit diag = do
                            }
                             in Map.insert x m Map.empty) $ labNodes diag
  return (sig, mors)
+
+convertBasicTheory :: (Sign.Sign, [AS_Anno.Named AS.TEXT_META]) -> AS.BASIC_SPEC
+convertBasicTheory (_, l) =
+  AS.Basic_spec $
+    map AS_Anno.emptyAnno $
+      [AS.Axiom_items $ map (AS_Anno.emptyAnno . AS_Anno.sentence) $ l]
diff --git a/CommonLogic/Logic_CommonLogic.hs b/CommonLogic/Logic_CommonLogic.hs
index 55ffc5c6ed..f6fe64dd4e 100644
--- a/CommonLogic/Logic_CommonLogic.hs
+++ b/CommonLogic/Logic_CommonLogic.hs
@@ -136,6 +136,7 @@ instance StaticAnalysis CommonLogic
       morphism_union CommonLogic = ()
 -}
       signature_colimit CommonLogic = signColimit
+      convertTheory CommonLogic = Just convertBasicTheory
 
 
 -- | Sublogics