# HG changeset patch
# User paulson
# Date 825671857 -3600
# Node ID 608dd813b4377346e440d23296ec278e36c6f56a
# Parent  bfbadb70d79405f62e131c06a10ee8f972fc908c
Theories are now in theory.ML

diff -r bfbadb70d794 -r 608dd813b437 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Feb 29 18:54:46 1996 +0100
+++ b/src/Pure/ROOT.ML	Fri Mar 01 10:17:37 1996 +0100
@@ -33,6 +33,7 @@
 use "unify.ML";
 use "net.ML";
 use "logic.ML";
+use "theory.ML";
 use "thm.ML";
 use "drule.ML";
 use "tctical.ML";
@@ -40,8 +41,8 @@
 use "goals.ML";
 use "axclass.ML";
 
-structure Pure = struct val thy = pure_thy end;
-structure CPure = struct val thy = cpure_thy end;
+structure Pure  = struct val thy = Theory.pure_thy end;
+structure CPure = struct val thy = Theory.cpure_thy end;
 
 (*Theory parser and loader*)
 cd "Thy";
diff -r bfbadb70d794 -r 608dd813b437 src/Pure/install_pp.ML
--- a/src/Pure/install_pp.ML	Thu Feb 29 18:54:46 1996 +0100
+++ b/src/Pure/install_pp.ML	Fri Mar 01 10:17:37 1996 +0100
@@ -6,8 +6,8 @@
 
 fun init_pps () =
   use_string
-   ["install_pp (make_pp [\"Thm\", \"thm\"] pprint_thm);",
-    "install_pp (make_pp [\"Thm\", \"theory\"] pprint_theory);",
+   ["install_pp (make_pp [\"Theory\", \"theory\"] pprint_theory);",
+    "install_pp (make_pp [\"Thm\", \"thm\"] pprint_thm);",
     "install_pp (make_pp [\"Thm\", \"cterm\"] pprint_cterm);",
     "install_pp (make_pp [\"Thm\", \"ctyp\"] pprint_ctyp);",
     "install_pp (make_pp [\"Sign\", \"sg\"] Sign.pprint_sg);",