src/Pure/ROOT.ML
changeset 49041 9edfd36a0355
parent 48990 12814717c95c
child 49560 11430dd89e35
     1.1 --- a/src/Pure/ROOT.ML	Fri Aug 31 15:24:26 2012 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Fri Aug 31 15:25:26 2012 +0200
     1.3 @@ -158,11 +158,19 @@
     1.4  use "conjunction.ML";
     1.5  use "assumption.ML";
     1.6  use "display.ML";
     1.7 -use "goal.ML";
     1.8  
     1.9  
    1.10  (* Isar -- Intelligible Semi-Automated Reasoning *)
    1.11  
    1.12 +(*ML support*)
    1.13 +use "ML/ml_syntax.ML";
    1.14 +use "ML/ml_env.ML";
    1.15 +use "Isar/runtime.ML";
    1.16 +use "ML/ml_compiler.ML";
    1.17 +if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
    1.18 +
    1.19 +use "goal.ML";
    1.20 +
    1.21  (*proof context*)
    1.22  use "Isar/object_logic.ML";
    1.23  use "Isar/rule_cases.ML";
    1.24 @@ -185,13 +193,6 @@
    1.25  use "Isar/keyword.ML";
    1.26  use "Isar/parse.ML";
    1.27  use "Isar/args.ML";
    1.28 -
    1.29 -(*ML support*)
    1.30 -use "ML/ml_syntax.ML";
    1.31 -use "ML/ml_env.ML";
    1.32 -use "Isar/runtime.ML";
    1.33 -use "ML/ml_compiler.ML";
    1.34 -if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
    1.35  use "ML/ml_context.ML";
    1.36  
    1.37  (*theory sources*)