load proof term operations later;

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

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