src/Pure/ML/ml_test.ML
changeset 31327 ffa5356cc343
parent 31318 133d1cfd6ae7
child 31328 0d3aa0aeb96f
--- a/src/Pure/ML/ml_test.ML	Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Pure/ML/ml_test.ML	Mon Jun 01 15:26:00 2009 +0200
@@ -24,7 +24,7 @@
 );
 
 fun inherit_env context =
-  ML_Context.inherit_env context #>
+  ML_Env.inherit context #>
   Extra_Env.put (Extra_Env.get context);
 
 fun register_tokens toks context =
@@ -155,7 +155,7 @@
         error (output ()); raise exn);
   in if verbose then print (output ()) else () end;
 
-val eval = use_text ML_Context.local_context;
+val eval = use_text ML_Env.local_context;
 
 
 (* ML test command *)