src/Pure/context.ML

   val setmp: theory option -> ('a -> 'b) -> 'a -> 'b
   val pass: theory option -> ('a -> 'b) -> 'a -> 'b * theory option
   val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
   val save: ('a -> 'b) -> 'a -> 'b
   val >> : (theory -> theory) -> unit
+  val ml_output: (string -> unit) * (string -> unit)
   val use_mltext: string -> bool -> theory option -> unit
   val use_mltext_theory: string -> bool -> theory -> theory
   val use_let: string -> string -> string -> theory -> theory
   val use_setup: string -> theory -> theory
 end;

 fun >> f = set_context (Some (f (the_context ())));
 
 
 (* use ML text *)
 
-fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_text priority verb txt) ();
-fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_text priority verb) txt);
+val ml_output = (writeln, error_msg: string -> unit);
+
+fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_text ml_output verb txt) ();
+fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_text ml_output verb) txt);
 
 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
 
 fun use_let bind body txt =
   use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");