src/Pure/RAW/ROOT_polyml.ML

--- a/src/Pure/RAW/ROOT_polyml.ML	Tue Mar 01 21:10:29 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Tue Mar 01 22:11:36 2016 +0100
@@ -167,7 +167,7 @@
 then use "RAW/ml_compiler_parameters_polyml-5.6.ML" else ();
 
 use "RAW/ml_positions.ML";
-use "RAW/compiler_polyml.ML";
+use "RAW/ml_compiler0.ML";
 
 PolyML.Compiler.reportUnreferencedIds := true;
 PolyML.Compiler.printInAlphabeticalOrder := false;