--- 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";
--- 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);",