tuned;

--- a/src/Pure/ML-Systems/ml_debugger.ML	Thu Aug 06 11:46:47 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger.ML	Thu Aug 06 14:23:59 2015 +0200
@@ -1,21 +1,21 @@
 (*  Title:      Pure/ML/ml_debugger.ML
     Author:     Makarius
 
-ML debugger interface.
+ML debugger interface -- dummy version.
 *)
 
 signature ML_DEBUGGER =
 sig
-  val on_entry: (string * 'a -> unit) option -> unit
-  val on_exit: (string * 'a -> unit) option -> unit
-  val on_exit_exception: (string * 'a -> exn -> unit) option -> unit
-  val on_breakpoint: ('a * bool Unsynchronized.ref -> unit) option -> unit
+  val on_entry: (string * 'location -> unit) option -> unit
+  val on_exit: (string * 'location -> unit) option -> unit
+  val on_exit_exception: (string * 'location -> exn -> unit) option -> unit
+  val on_breakpoint: ('location * bool Unsynchronized.ref -> unit) option -> unit
   type state
   val state: Thread.thread -> state list
   val debug_function: state -> string
   val debug_function_arg: state -> ML_Name_Space.valueVal
   val debug_function_result: state -> ML_Name_Space.valueVal
-  val debug_location: state -> 'a
+  val debug_location: state -> 'location
   val debug_name_space: state -> ML_Name_Space.T
 end;
 
@@ -24,7 +24,6 @@
 
 (* hooks *)
 
-type location = unit;
 fun on_entry _ = ();
 fun on_exit _ = ();
 fun on_exit_exception _ = ();

--- a/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Thu Aug 06 11:46:47 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Thu Aug 06 14:23:59 2015 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/ml_debugger_polyml-5.5.3.ML
     Author:     Makarius
 
-ML debugger interface -- Poly/ML 5.5.3, or later.
+ML debugger interface -- for Poly/ML 5.5.3, or later.
 *)
 
 signature ML_DEBUGGER =