src/Pure/ROOT.ML
changeset 53192 04df1d236e1c
parent 52926 6415d95bf7a2
child 53212 387b9f7cb0ac
--- a/src/Pure/ROOT.ML	Sun Aug 25 17:17:48 2013 +0200
+++ b/src/Pure/ROOT.ML	Sun Aug 25 20:32:26 2013 +0200
@@ -185,6 +185,9 @@
 if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
 if ML_System.name = "polyml-5.5.1" then use "ML/exn_trace_polyml-5.5.1.ML" else ();
 
+(*global execution*)
+use "PIDE/document_id.ML";
+use "PIDE/execution.ML";
 use "skip_proof.ML";
 use "goal.ML";
 
@@ -257,7 +260,6 @@
 
 (*toplevel transactions*)
 use "Isar/proof_node.ML";
-use "PIDE/document_id.ML";
 use "Isar/toplevel.ML";
 
 (*theory documents*)
@@ -267,7 +269,6 @@
 use "Isar/outer_syntax.ML";
 use "General/graph_display.ML";
 use "Thy/present.ML";
-use "PIDE/execution.ML";
 use "PIDE/command.ML";
 use "PIDE/query_operation.ML";
 use "Thy/thy_load.ML";