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