# HG changeset patch
# User wenzelm
# Date 901719488 -7200
# Node ID c02b0c72778055f910e0bddffea2fad2b60f4b7c
# Parent  54aaa779b6b4516de45ff6686afc21b297c7e94f
late setup of Pure and CPure;

diff -r 54aaa779b6b4 -r c02b0c727780 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Jul 28 17:05:34 1998 +0200
+++ b/src/Pure/ROOT.ML	Wed Jul 29 15:38:08 1998 +0200
@@ -46,13 +46,14 @@
 use "tactic.ML";
 use "goals.ML";
 use "axclass.ML";
-use "pure.ML";
 
 (*theory parser and loader*)
 cd "Thy";
 use "ROOT.ML";
 cd "..";
 
+use "pure.ML";
+
 use "install_pp.ML";
 
 (*if true then some packages won't be too serious about actually proving things*)
diff -r 54aaa779b6b4 -r c02b0c727780 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Jul 28 17:05:34 1998 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Jul 29 15:38:08 1998 +0200
@@ -36,6 +36,7 @@
 signature THY_INFO =
 sig
   include BASIC_THY_INFO
+  val mk_info: string * string list * string list * theory -> string * thy_info
   val loaded_thys: thy_info Symtab.table ref
   val get_thyinfo: string -> thy_info option
   val store_theory: theory -> unit
@@ -58,11 +59,7 @@
     thy_time = Some "", ml_time = Some "", theory = Some theory}: thy_info);
 
 (*preloaded theories*)
-val loaded_thys =
-  ref (Symtab.make (map mk_info
-    [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
-     ("Pure", [], ["ProtoPure"], Pure.thy),
-     ("CPure", [], ["ProtoPure"], CPure.thy)]));
+val loaded_thys = ref (Symtab.empty: thy_info Symtab.table);
 
 
 (* retrieve info *)
diff -r 54aaa779b6b4 -r c02b0c727780 src/Pure/pure.ML
--- a/src/Pure/pure.ML	Tue Jul 28 17:05:34 1998 +0200
+++ b/src/Pure/pure.ML	Wed Jul 29 15:38:08 1998 +0200
@@ -2,26 +2,27 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-The actual Pure and CPure theories.
+Setup the actual Pure and CPure theories.
 *)
 
 structure Pure =
 struct
-
-val thy =
-  PureThy.begin_theory "Pure" [ProtoPure.thy]
-  |> Theory.add_syntax Syntax.pure_appl_syntax
-  |> PureThy.end_theory;
-
+  val thy =
+    PureThy.begin_theory "Pure" [ProtoPure.thy]
+    |> Theory.add_syntax Syntax.pure_appl_syntax
+    |> PureThy.end_theory;
 end;
 
-
 structure CPure =
 struct
+  val thy =
+    PureThy.begin_theory "CPure" [ProtoPure.thy]
+    |> Theory.add_syntax Syntax.pure_applC_syntax
+    |> PureThy.end_theory;
+end;
 
-val thy =
-  PureThy.begin_theory "CPure" [ProtoPure.thy]
-  |> Theory.add_syntax Syntax.pure_applC_syntax
-  |> PureThy.end_theory;
-
-end;
+ThyInfo.loaded_thys :=
+  (Symtab.make (map ThyInfo.mk_info
+    [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
+     ("Pure", [], ["ProtoPure"], Pure.thy),
+     ("CPure", [], ["ProtoPure"], CPure.thy)]));