src/Pure/codegen.ML

               Pretty.block [str "SOME ", Pretty.block (str "[" ::
                 Pretty.commas (map (fn (s, _) => str (s ^ "_t ()")) args) @
                   [str "]"])]]),
           str ");"]) ^
       "\n\nend;\n";
-    val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
+    val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
     val dummy_report = ([], false)
   in (fn size => (! test_fn size, dummy_report)) end;
 
 
 

               mk_app false (mk_term_of gr "Generated" false (fastype_of t))
                 [str "(result ())"],
               str ");"]) ^
           "\n\nend;\n";
         val _ = NAMED_CRITICAL "codegen" (fn () =>   (* FIXME ??? *)
-          ML_Context.eval_in (SOME ctxt) false Position.none s);
+          ML_Context.eval_text_in (SOME ctxt) false Position.none s);
       in !eval_result end;
   in e () end;
 
 val (_, evaluation_conv) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (Binding.name "evaluation", fn ct =>

     let
       val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
       val (code, gr) = setmp_CRITICAL mode mode'' (generate_code thy modules module) xs;
       val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>
         (case opt_fname of
-          NONE => ML_Context.eval false Position.none (cat_lines (map snd code))
+          NONE => ML_Context.eval_text false Position.none (cat_lines (map snd code))
         | SOME fname =>
             if lib then app (fn (name, s) => File.write
                 (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s)
               (("ROOT", implode (map (fn (name, _) =>
                   "use \"" ^ name ^ ".ML\";\n") code)) :: code)