# HG changeset patch
# User wenzelm
# Date 918056857 -3600
# Node ID a42dbf1af868f7e7c808e14bad1e49d33cb73c72
# Parent  381b27ca05439572a7613ff7b349a432c0b5bce5
proper setup of preloaded theories (ThyInfo.register_theory);

diff -r 381b27ca0543 -r a42dbf1af868 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;