--- a/src/Pure/RAW/ROOT_polyml.ML Tue Mar 01 17:26:53 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML Tue Mar 01 19:42:59 2016 +0100
@@ -164,7 +164,6 @@
if ML_System.name = "polyml-5.6"
then use "RAW/ml_compiler_parameters_polyml-5.6.ML" else ();
-use "RAW/use_context.ML";
use "RAW/ml_positions.ML";
use "RAW/compiler_polyml.ML";
@@ -186,5 +185,5 @@
(* ML debugger *)
if ML_System.name = "polyml-5.6"
-then use "RAW/ml_debugger_polyml-5.6.ML"
-else use "RAW/ml_debugger.ML";
+then use_no_debug "RAW/ml_debugger_polyml-5.6.ML"
+else use_no_debug "RAW/ml_debugger.ML";