src/Pure/ML-Systems/ml_debugger.ML

--- a/src/Pure/ML-Systems/ml_debugger.ML	Mon Dec 21 15:09:35 2015 +0100
+++ b/src/Pure/ML-Systems/ml_debugger.ML	Mon Dec 21 15:46:23 2015 +0100
@@ -21,6 +21,7 @@
   val debug_function_result: state -> ML_Name_Space.valueVal
   val debug_location: state -> 'location
   val debug_name_space: state -> ML_Name_Space.T
+  val debug_local_name_space: state -> ML_Name_Space.T
 end;
 
 structure ML_Debugger: ML_DEBUGGER =
@@ -58,5 +59,6 @@
 fun debug_function_result () = fail ();
 fun debug_location () = fail ();
 fun debug_name_space () = fail ();
+fun debug_local_name_space () = fail ();
 
 end;