proper setup of preloaded theories (ThyInfo.register_theory);
authorwenzelm
Wed, 03 Feb 1999 16:47:37 +0100
changeset 6192 a42dbf1af868
parent 6191 381b27ca0543
child 6193 451d3d6c088f
proper setup of preloaded theories (ThyInfo.register_theory);
src/Pure/pure.ML
--- a/src/Pure/pure.ML	Wed Feb 03 16:46:56 1999 +0100
+++ b/src/Pure/pure.ML	Wed Feb 03 16:47:37 1999 +0100
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Setup the actual Pure and CPure theories.
+Final setup of the Pure theories.
 *)
 
 local
@@ -33,8 +33,6 @@
   end;
 end;
 
-ThyInfo.loaded_thys :=
-  (Symtab.make (map ThyInfo.mk_info
-    [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
-     ("Pure", [], ["ProtoPure"], Pure.thy),
-     ("CPure", [], ["ProtoPure"], CPure.thy)]));
+ThyInfo.register_theory ProtoPure.thy;
+ThyInfo.register_theory Pure.thy;
+ThyInfo.register_theory CPure.thy;