src/Pure/codegen.ML

                      mk_app false (mk_term_of gr "Generated" false T)
                        [Pretty.str s'], Pretty.str ")"]]) frees')) @
                   [Pretty.str "]"])]],
             Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
       "\n\nend;\n") ();
-    val _ = use_text Context.ml_output false s;
+    val _ = use_text Output.ml_output false s;
     fun iter f k = if k > i then NONE
       else (case (f () handle Match =>
           (warning "Exception Match raised in generated code"; NONE)) of
         NONE => iter f (k+1) | SOME x => SOME x);
     fun test k = if k > sz then NONE

           Pretty.brk 1,
           mk_app false (mk_term_of gr "Generated" false (fastype_of t))
             [Pretty.str "result"],
           Pretty.str ";"])  ^
       "\n\nend;\n";
-    val _ = use_text Context.ml_output false s
+    val _ = use_text Output.ml_output false s
   in !eval_result end);
 
 fun print_evaluated_term s = Toplevel.keep (fn state =>
   let
     val state' = Toplevel.enter_forward_proof state;

   (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
      let
        val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
        val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
      in ((case opt_fname of
-         NONE => use_text Context.ml_output false
+         NONE => use_text Output.ml_output false
            (space_implode "\n" (map snd code))
        | SOME fname =>
            if lib then
              app (fn (name, s) => File.write
                  (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s)