src/Pure/ROOT.ML
changeset 62355 00f7618a9f2b
parent 62354 fdd6989cc8a0
child 62356 e307a410f46c
--- a/src/Pure/ROOT.ML	Wed Feb 17 23:06:24 2016 +0100
+++ b/src/Pure/ROOT.ML	Wed Feb 17 23:15:47 2016 +0100
@@ -98,7 +98,7 @@
 
 (* concurrency within the ML runtime *)
 
-use "ML/exn_properties_polyml.ML";
+use "ML/exn_properties.ML";
 
 if ML_System.name = "polyml-5.5.0"
   orelse ML_System.name = "polyml-5.5.1"
@@ -200,11 +200,11 @@
 use "ML/ml_syntax.ML";
 use "ML/ml_env.ML";
 use "ML/ml_options.ML";
-use "ML/exn_output_polyml.ML";
+use "ML/exn_output.ML";
 use "ML/ml_options.ML";
 use "Isar/runtime.ML";
 use "PIDE/execution.ML";
-use "ML/ml_compiler_polyml.ML";
+use "ML/ml_compiler.ML";
 
 use "skip_proof.ML";
 use "goal.ML";