src/Pure/ROOT.ML
changeset 56206 7adec2a527f5
parent 56205 ceb8a93460b7
child 56208 06cc31dff138
--- a/src/Pure/ROOT.ML	Tue Mar 18 16:16:28 2014 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 18 16:44:51 2014 +0100
@@ -211,12 +211,6 @@
 use "Syntax/syntax_phases.ML";
 use "Isar/local_defs.ML";
 
-(*proof term operations*)
-use "Proof/reconstruct.ML";
-use "Proof/proof_syntax.ML";
-use "Proof/proof_rewrite_rules.ML";
-use "Proof/proof_checker.ML";
-
 (*outer syntax*)
 use "Isar/token.ML";
 use "Isar/keyword.ML";
@@ -271,6 +265,13 @@
 use "Isar/proof_node.ML";
 use "Isar/toplevel.ML";
 
+(*proof term operations*)
+use "Proof/reconstruct.ML";
+use "Proof/proof_syntax.ML";
+use "Proof/proof_rewrite_rules.ML";
+use "Proof/proof_checker.ML";
+use "Proof/extraction.ML";
+
 (*theory documents*)
 use "System/isabelle_system.ML";
 use "Thy/term_style.ML";
@@ -290,8 +291,6 @@
 
 use "subgoal.ML";
 
-use "Proof/extraction.ML";
-
 
 (* Isabelle/Isar system *)