--- a/src/Pure/ML/ml_env.ML Tue Mar 01 21:10:29 2016 +0100
+++ b/src/Pure/ML/ml_env.ML Tue Mar 01 22:11:36 2016 +0100
@@ -14,7 +14,7 @@
val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
- val local_context: use_context
+ val local_context: ML_Compiler0.context
val local_name_space: ML_Name_Space.T
val check_functor: string -> unit
end
@@ -162,7 +162,7 @@
allFunct = all #6 #allFunct}
end;
-val local_context: use_context =
+val local_context: ML_Compiler0.context =
{name_space = name_space {SML = false, exchange = false},
here = Position.here oo Position.line_file,
print = writeln,