src/Pure/ROOT.ML
changeset 62355 00f7618a9f2b
parent 62354 fdd6989cc8a0
child 62356 e307a410f46c
     1.1 --- a/src/Pure/ROOT.ML	Wed Feb 17 23:06:24 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Wed Feb 17 23:15:47 2016 +0100
     1.3 @@ -98,7 +98,7 @@
     1.4  
     1.5  (* concurrency within the ML runtime *)
     1.6  
     1.7 -use "ML/exn_properties_polyml.ML";
     1.8 +use "ML/exn_properties.ML";
     1.9  
    1.10  if ML_System.name = "polyml-5.5.0"
    1.11    orelse ML_System.name = "polyml-5.5.1"
    1.12 @@ -200,11 +200,11 @@
    1.13  use "ML/ml_syntax.ML";
    1.14  use "ML/ml_env.ML";
    1.15  use "ML/ml_options.ML";
    1.16 -use "ML/exn_output_polyml.ML";
    1.17 +use "ML/exn_output.ML";
    1.18  use "ML/ml_options.ML";
    1.19  use "Isar/runtime.ML";
    1.20  use "PIDE/execution.ML";
    1.21 -use "ML/ml_compiler_polyml.ML";
    1.22 +use "ML/ml_compiler.ML";
    1.23  
    1.24  use "skip_proof.ML";
    1.25  use "goal.ML";