src/Pure/ROOT.ML
changeset 5834 c6fea8488ce7
parent 5684 9a3acc4c7c2e
child 6038 dfdb7584cf96
--- a/src/Pure/ROOT.ML	Mon Nov 09 15:35:38 1998 +0100
+++ b/src/Pure/ROOT.ML	Mon Nov 09 15:36:27 1998 +0100
@@ -10,7 +10,6 @@
 val version = "Isabelle repository";
 
 print_depth 1;
-ml_prompts "> " "# ";
 
 (*fake hiding of private structures*)
 structure Hidden = struct end;
@@ -37,6 +36,7 @@
 use "logic.ML";
 use "theory.ML";
 use "theory_data.ML";
+use "object_logic.ML";
 use "thm.ML";
 use "display.ML";
 use "attribute.ML";
@@ -55,6 +55,11 @@
 use "ROOT.ML";
 cd "..";
 
+(*the Isar subsystem*)
+cd "Isar";
+use "ROOT.ML";
+cd "..";
+
 use "pure.ML";
 
 use "install_pp.ML";
@@ -75,3 +80,4 @@
 open Use;
 
 print_depth 8;
+(*ml_prompts "ML> " "ML# ";*)