src/Pure/ROOT.ML
changeset 49041 9edfd36a0355
parent 48990 12814717c95c
child 49560 11430dd89e35
--- a/src/Pure/ROOT.ML	Fri Aug 31 15:24:26 2012 +0200
+++ b/src/Pure/ROOT.ML	Fri Aug 31 15:25:26 2012 +0200
@@ -158,11 +158,19 @@
 use "conjunction.ML";
 use "assumption.ML";
 use "display.ML";
-use "goal.ML";
 
 
 (* Isar -- Intelligible Semi-Automated Reasoning *)
 
+(*ML support*)
+use "ML/ml_syntax.ML";
+use "ML/ml_env.ML";
+use "Isar/runtime.ML";
+use "ML/ml_compiler.ML";
+if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
+
+use "goal.ML";
+
 (*proof context*)
 use "Isar/object_logic.ML";
 use "Isar/rule_cases.ML";
@@ -185,13 +193,6 @@
 use "Isar/keyword.ML";
 use "Isar/parse.ML";
 use "Isar/args.ML";
-
-(*ML support*)
-use "ML/ml_syntax.ML";
-use "ML/ml_env.ML";
-use "Isar/runtime.ML";
-use "ML/ml_compiler.ML";
-if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
 use "ML/ml_context.ML";
 
 (*theory sources*)