# HG changeset patch
# User wenzelm
# Date 1213808102 -7200
# Node ID 0f8106808e66136fa6b83ea190265f1866464523
# Parent  ffbe8b4ebd229718b615cf0af6621b0a9f621fe4
load proof term operations later;

diff -r ffbe8b4ebd22 -r 0f8106808e66 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Wed Jun 18 18:55:01 2008 +0200
+++ b/src/Pure/Isar/ROOT.ML	Wed Jun 18 18:55:02 2008 +0200
@@ -13,6 +13,12 @@
 use "proof_context.ML";
 use "local_defs.ML";
 
+(*proof term operations*)
+use "../Proof/reconstruct.ML";
+use "../Proof/proof_syntax.ML";
+use "../Proof/proof_rewrite_rules.ML";
+use "../Proof/proofchecker.ML";
+
 (*outer syntax*)
 use "outer_lex.ML";
 use "args.ML";
diff -r ffbe8b4ebd22 -r 0f8106808e66 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Jun 18 18:55:01 2008 +0200
+++ b/src/Pure/ROOT.ML	Wed Jun 18 18:55:02 2008 +0200
@@ -77,12 +77,6 @@
 use "goal.ML";
 use "axclass.ML";
 
-(*proof term operations*)
-use "Proof/reconstruct.ML";
-use "Proof/proof_syntax.ML";
-use "Proof/proof_rewrite_rules.ML";
-use "Proof/proofchecker.ML";
-
 (*the main Isar system*)
 cd "Isar"; use "ROOT.ML"; cd "..";
 use "subgoal.ML";