--- a/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML Thu Jul 16 11:10:57 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML Thu Jul 16 11:38:18 2015 +0200
@@ -7,12 +7,6 @@
structure ML_Debugger: ML_DEBUGGER =
struct
-(* compiler parameters *)
-
-type compiler_parameters = PolyML.Compiler.compilerParameters;
-val compiler_parameters = PolyML.Compiler.CPDebug true;
-
-
(* hooks *)
type location = PolyML.location;
@@ -35,3 +29,6 @@
val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
end;
+
+fun ml_debugger_parameters false = []
+ | ml_debugger_parameters true = [PolyML.Compiler.CPDebug true];