--- a/src/Pure/ROOT.ML Thu Apr 21 22:00:28 2005 +0200
+++ b/src/Pure/ROOT.ML Thu Apr 21 22:02:06 2005 +0200
@@ -63,7 +63,7 @@
use "codegen.ML";
use "Proof/extraction.ML";
-(*old-style goal package*)
+(*old goal package -- obsolete*)
use "goals.ML";
(*the IsaPlanner subsystem*)
@@ -72,8 +72,10 @@
(*configuration for Proof General*)
use "proof_general.ML";
-(*final Pure theory setup*)
-use "pure.ML";
+(*the Pure theories*)
+use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end;
+use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end;
+
(*several object-logics declare theories that hide basis library structures*)
structure BasisLibrary =