# HG changeset patch
# User wenzelm
# Date 1221679664 -7200
# Node ID 8dab53900e8ca3255eb1e919b64560017a74dc11
# Parent  9873697fa411829a1a4e9d075a3f249a5e38e104
ML_Context.evaluate: proper context (for ML environment);
use_text/use_file now depend on explicit ML name space;

diff -r 9873697fa411 -r 8dab53900e8c src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Wed Sep 17 21:27:43 2008 +0200
+++ b/src/Tools/code/code_ml.ML	Wed Sep 17 21:27:44 2008 +0200
@@ -886,6 +886,7 @@
 
 fun eval eval'' term_of reff thy ct args =
   let
+    val ctxt = ProofContext.init thy;
     val _ = if null (term_frees (term_of ct)) then () else error ("Term "
       ^ quote (Syntax.string_of_term_global thy (term_of ct))
       ^ " to be evaluated contains free variables");
@@ -899,7 +900,7 @@
         val (value_code, [value_name']) = ml_code_of thy program' [Code_Name.value_name];
         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
-      in ML_Context.evaluate Output.ml_output false reff sml_code end;
+      in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end;
   in eval'' thy (fn t => (t, eval')) ct end;
 
 fun eval_conv reff = eval Code_Thingol.eval_conv Thm.term_of reff;
@@ -966,7 +967,8 @@
 
 fun isar_seri_sml module_name =
   Code_Target.parse_args (Scan.succeed ())
-  #> (fn () => serialize_ml target_SML (SOME (use_text (1, "generated code") Output.ml_output false))
+  #> (fn () => serialize_ml target_SML
+      (SOME (use_text ML_Context.name_space (1, "generated code") Output.ml_output false))
       pr_sml_module pr_sml_stmt module_name);
 
 fun isar_seri_ocaml module_name =