# HG changeset patch
# User wenzelm
# Date 1169240896 -3600
# Node ID d76ea9928959a3093d039fb278c311ab1f306919
# Parent  926afa3361e11b3868ad7afdb46317898009312f
tuned order;

diff -r 926afa3361e1 -r d76ea9928959 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Jan 19 22:08:15 2007 +0100
+++ b/src/Pure/ROOT.ML	Fri Jan 19 22:08:16 2007 +0100
@@ -67,14 +67,7 @@
 use "Proof/proof_rewrite_rules.ML";
 use "Proof/proofchecker.ML";
 
-(*theory auto loader database*)
-use "Thy/thy_load.ML";
-use "Thy/thy_info.ML";
-
-(*theory syntax*)
-use "Isar/outer_lex.ML";
-
-(*the Isar system*)
+(*the main Isar system*)
 cd "Isar"; use "ROOT.ML"; cd "..";
 use "subgoal.ML";