--- a/src/Pure/ML-Systems/ml_debugger_dummy.ML Thu Jul 16 11:10:57 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger_dummy.ML Thu Jul 16 11:38:18 2015 +0200
@@ -6,8 +6,6 @@
signature ML_DEBUGGER =
sig
- type compiler_parameters
- val compiler_parameters: compiler_parameters
type location
val on_entry: (string * location -> unit) option -> unit
val on_exit: (string * location -> unit) option -> unit
@@ -25,12 +23,6 @@
structure ML_Debugger: ML_DEBUGGER =
struct
-(* compiler parameters *)
-
-type compiler_parameters = unit;
-val compiler_parameters = ();
-
-
(* hooks *)
type location = unit;
@@ -54,3 +46,6 @@
fun debug_name_space () = fail ();
end;
+
+
+fun ml_debugger_parameters (_: bool) = [];