# HG changeset patch
# User wenzelm
# Date 1414751801 -3600
# Node ID 521cea5fa777c3a70b0faa2193ea33a08ecddeac
# Parent  22b87ab47d3b45116415142f8ca7e17914a7fc06
discontinued obsolete Output.urgent_message;

diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Library/refute.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -1068,31 +1068,31 @@
                             ". Available solvers: " ^
                             commas (map (quote o fst) (SAT_Solver.get_solvers ())) ^ ".")
           in
-            Output.urgent_message "Invoking SAT solver...";
+            writeln "Invoking SAT solver...";
             (case solver fm of
               SAT_Solver.SATISFIABLE assignment =>
-                (Output.urgent_message ("Model found:\n" ^ print_model ctxt model
+                (writeln ("Model found:\n" ^ print_model ctxt model
                   (fn i => case assignment i of SOME b => b | NONE => true));
                  if maybe_spurious then "potential" else "genuine")
             | SAT_Solver.UNSATISFIABLE _ =>
-                (Output.urgent_message "No model exists.";
+                (writeln "No model exists.";
                 case next_universe universe sizes minsize maxsize of
                   SOME universe' => find_model_loop universe'
-                | NONE => (Output.urgent_message
+                | NONE => (writeln
                     "Search terminated, no larger universe within the given limits.";
                     "none"))
             | SAT_Solver.UNKNOWN =>
-                (Output.urgent_message "No model found.";
+                (writeln "No model found.";
                 case next_universe universe sizes minsize maxsize of
                   SOME universe' => find_model_loop universe'
-                | NONE => (Output.urgent_message
+                | NONE => (writeln
                   "Search terminated, no larger universe within the given limits.";
                   "unknown"))) handle SAT_Solver.NOT_CONFIGURED =>
               (error ("SAT solver " ^ quote satsolver ^ " is not configured.");
                "unknown")
           end
           handle MAXVARS_EXCEEDED =>
-            (Output.urgent_message ("Search terminated, number of Boolean variables ("
+            (writeln ("Search terminated, number of Boolean variables ("
               ^ string_of_int maxvars ^ " allowed) exceeded.");
               "unknown")
 
@@ -1114,14 +1114,14 @@
     maxtime>=0 orelse
       error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
     (* enter loop with or without time limit *)
-    Output.urgent_message ("Trying to find a model that "
+    writeln ("Trying to find a model that "
       ^ (if negate then "refutes" else "satisfies") ^ ": "
       ^ Syntax.string_of_term ctxt t);
     if maxtime > 0 then (
       TimeLimit.timeLimit (Time.fromSeconds maxtime)
         wrapper ()
       handle TimeLimit.TimeOut =>
-        (Output.urgent_message ("Search terminated, time limit (" ^
+        (writeln ("Search terminated, time limit (" ^
             string_of_int maxtime
             ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
          check_expect "unknown")
@@ -1207,7 +1207,7 @@
     val t = th |> prop_of
   in
     if Logic.count_prems t = 0 then
-      (Output.urgent_message "No subgoal!"; "none")
+      (writeln "No subgoal!"; "none")
     else
       let
         val assms = map term_of (Assumption.all_assms_of ctxt)
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -428,7 +428,7 @@
           |> tap (fn factss =>
                      "Line " ^ str0 (Position.line_of pos) ^ ": " ^
                      Sledgehammer.string_of_factss factss
-                     |> Output.urgent_message)
+                     |> writeln)
         val prover = get_prover ctxt prover_name params goal facts
         val problem =
           {comment = "", state = st', goal = goal, subgoal = i,
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -171,7 +171,7 @@
   let
     val params = []
     val res = Refute.refute_term (Proof_Context.init_global thy) params [] t
-    val _ = Output.urgent_message ("Refute: " ^ res)
+    val _ = writeln ("Refute: " ^ res)
   in
     (rpair []) (case res of
       "genuine" => GenuineCex
@@ -194,7 +194,7 @@
     val state = Proof.init ctxt
     val (res, _) = Nitpick.pick_nits_in_term state
       (Nitpick_Commands.default_params thy []) Nitpick.Normal 1 1 1 [] [] [] t
-    val _ = Output.urgent_message ("Nitpick: " ^ res)
+    val _ = writeln ("Nitpick: " ^ res)
   in
     (rpair []) (case res of
       "genuine" => GenuineCex
@@ -343,21 +343,21 @@
 (*
 fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   let
-    val _ = Output.urgent_message ("Invoking " ^ mtd_name)
+    val _ = writeln ("Invoking " ^ mtd_name)
     val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t
       handle ERROR s => (tracing s; (Error, ([], NONE))))
-    val _ = Output.urgent_message (" Done")
+    val _ = writeln (" Done")
   in (res, (time :: timing, reports)) end
 *)  
 fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   let
-    val _ = Output.urgent_message ("Invoking " ^ mtd_name)
+    val _ = writeln ("Invoking " ^ mtd_name)
     val (res, timing) = elapsed_time "total time"
       (fn () => case try (invoke_mtd thy) t of
           SOME (res, _) => res
-        | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
+        | NONE => (writeln ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
             Error))
-    val _ = Output.urgent_message (" Done")
+    val _ = writeln (" Done")
   in (res, [timing]) end
 
 (* creating entries *)
@@ -387,7 +387,7 @@
     val mutants =
       if exec then
         let
-          val _ = Output.urgent_message ("BEFORE PARTITION OF " ^
+          val _ = writeln ("BEFORE PARTITION OF " ^
                             string_of_int (length mutants) ^ " MUTANTS")
           val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
           val _ = tracing ("AFTER PARTITION (" ^ string_of_int (length execs) ^
@@ -404,7 +404,7 @@
           |> filter (is_some o try (Thm.cterm_of thy))
           |> filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy)))
           |> take_random max_mutants
-    val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
+    val _ = map (fn t => writeln ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
   in
     create_entry thy thm exec mutants mtds
   end
@@ -458,7 +458,7 @@
 (* theory -> mtd list -> thm list -> string -> unit *)
 fun mutate_theorems_and_write_report thy (num_mutations, max_mutants) mtds thms file_name =
   let
-    val _ = Output.urgent_message "Starting Mutabelle..."
+    val _ = writeln "Starting Mutabelle..."
     val ctxt = Proof_Context.init_global thy
     val path = Path.explode file_name
     (* for normal report: *)
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -117,7 +117,7 @@
          if falsify then "CounterSatisfiable" else "Satisfiable"
        else
          "Unknown")
-      |> Output.urgent_message
+      |> writeln
     val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
     val params =
       [("maxtime", string_of_int timeout),
@@ -135,7 +135,7 @@
 
 fun SOLVE_TIMEOUT seconds name tac st =
   let
-    val _ = Output.urgent_message ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
+    val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
     val result =
       TimeLimit.timeLimit (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
       handle
@@ -143,8 +143,8 @@
       | ERROR _ => NONE
   in
     (case result of
-      NONE => (Output.urgent_message ("FAILURE: " ^ name); Seq.empty)
-    | SOME st' => (Output.urgent_message ("SUCCESS: " ^ name); Seq.single st'))
+      NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
+    | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
   end
 
 fun nitpick_finite_oracle_tac ctxt timeout i th =
@@ -264,7 +264,7 @@
   Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => @{prop False})
 
 fun print_szs_of_success conjs success =
-  Output.urgent_message ("% SZS status " ^
+  writeln ("% SZS status " ^
     (if success then
        if null conjs then "Unsatisfiable" else "Theorem"
      else
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -241,11 +241,11 @@
         o Pretty.mark Markup.information
       else
         print o Pretty.string_of
-    val pprint_a = pprint Output.urgent_message
-    fun pprint_nt f = () |> is_mode_nt mode ? pprint Output.urgent_message o f
-    fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f
+    val pprint_a = pprint writeln
+    fun pprint_nt f = () |> is_mode_nt mode ? pprint writeln o f
+    fun pprint_v f = () |> verbose ? pprint writeln o f
     fun pprint_d f = () |> debug ? pprint tracing o f
-    val print = pprint Output.urgent_message o curry Pretty.blk 0 o pstrs
+    val print = pprint writeln o curry Pretty.blk 0 o pstrs
     fun print_t f = () |> mode = TPTP ? print o f
 (*
     val print_g = pprint tracing o Pretty.str
@@ -1015,8 +1015,8 @@
 fun pick_nits_in_term state (params as {timeout, expect, ...}) mode i n step
                       subst def_assm_ts nondef_assm_ts orig_t =
   let
-    val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
-    val print_t = if mode = TPTP then Output.urgent_message else K ()
+    val print_nt = if is_mode_nt mode then writeln else K ()
+    val print_t = if mode = TPTP then writeln else K ()
   in
     if getenv "KODKODI" = "" then
       (* The "expect" argument is deliberately ignored if Kodkodi is missing so
@@ -1068,7 +1068,7 @@
     val t = state |> Proof.raw_goal |> #goal |> prop_of
   in
     case Logic.count_prems t of
-      0 => (Output.urgent_message "No subgoal!"; (noneN, state))
+      0 => (writeln "No subgoal!"; (noneN, state))
     | n =>
       let
         val t = Logic.goal_params t i |> fst
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -2140,8 +2140,7 @@
                     map (wf_constraint_for_triple rel) triples
                     |> foldr1 s_conj |> HOLogic.mk_Trueprop
          val _ = if debug then
-                   Output.urgent_message ("Wellfoundedness goal: " ^
-                             Syntax.string_of_term ctxt prop ^ ".")
+                   writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
                  else
                    ()
        in
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -1059,7 +1059,7 @@
           if debug then
             (if negate then "Genuineness" else "Spuriousness") ^ " goal: " ^
             Syntax.string_of_term ctxt prop ^ "."
-            |> Output.urgent_message
+            |> writeln
           else
             ()
         val goal = prop |> cterm_of thy |> Goal.init
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -360,7 +360,7 @@
 fun try_upto_depth ctxt f =
   let
     val max_depth = Config.get ctxt Quickcheck.depth
-    fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
+    fun message s = if Config.get ctxt Quickcheck.quiet then () else writeln s
     fun try' i =
       if i <= max_depth then
         let
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -221,8 +221,8 @@
 fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) =
   let
     val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
-    fun message s = if quiet then () else Output.urgent_message s
-    fun verbose_message s = if not quiet andalso verbose then Output.urgent_message s else ()
+    fun message s = if quiet then () else writeln s
+    fun verbose_message s = if not quiet andalso verbose then writeln s else ()
     val current_size = Unsynchronized.ref 0
     val current_result = Unsynchronized.ref Quickcheck.empty_result 
     val tmp_prefix = "Quickcheck_Narrowing"
@@ -511,7 +511,7 @@
         (maps (map snd) correct_inst_goals) []
     end
   else
-    (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message
+    (if Config.get ctxt Quickcheck.quiet then () else writeln
       ("Environment variable ISABELLE_GHC is not set. To use narrowing-based quickcheck, please set "
         ^ "this variable to your GHC Haskell compiler in your settings file. "
         ^ "To deactivate narrowing-based quickcheck, set quickcheck_narrowing_active to false.");
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Tools/Sledgehammer/async_manager.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -106,7 +106,7 @@
                   tool ^ ": " ^
                   implode_message (workers |> sort_distinct string_ord, work)
                   |> break_into_chunks
-                  |> List.app Output.urgent_message)
+                  |> List.app writeln)
 
 fun check_thread_manager () = Synchronized.change global_state
   (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
@@ -178,7 +178,7 @@
       val state' = make_state manager timeout_heap [] (killing @ canceling) messages store
       val _ =
         if null killing then ()
-        else Output.urgent_message ("Interrupted active " ^ das_wort_worker ^ "s.")
+        else writeln ("Interrupted active " ^ das_wort_worker ^ "s.")
     in state' end)
 
 fun str_of_time time = string_of_int (Time.toSeconds time) ^ " s"
@@ -210,7 +210,7 @@
       case map_filter canceling_info canceling of
         [] => []
       | ss => "Interrupting " ^ das_wort_worker ^ "s" :: ss
-  in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
+  in writeln (space_implode "\n\n" (running @ interrupting)) end
 
 fun thread_messages tool das_wort_worker opt_limit =
   let
@@ -222,6 +222,6 @@
         (if length tool_store <= limit then ":"
          else " (" ^ string_of_int limit ^ " displayed):")
     val ss = tool_store |> chop limit |> #1 |> map (op ^ o snd)
-  in List.app Output.urgent_message (header :: maps break_into_chunks ss) end
+  in List.app writeln (header :: maps break_into_chunks ss) end
 
 end;
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -137,7 +137,7 @@
       |> commas
       |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
                   " proof (of " ^ string_of_int (length facts) ^ "): ") "."
-      |> Output.urgent_message
+      |> writeln
 
     fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
         let
@@ -230,7 +230,7 @@
           else
             outcome
             |> Async_Manager.break_into_chunks
-            |> List.app Output.urgent_message
+            |> List.app writeln
       in (outcome_code, state) end
     else
       (Async_Manager.thread SledgehammerN birth_time death_time
@@ -259,12 +259,12 @@
   else
     (case subgoal_count state of
       0 =>
-      ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state)))
+      ((if blocking then error else writeln) "No subgoal!"; (false, (noneN, state)))
     | n =>
       let
         val _ = Proof.assert_backward state
         val print =
-          if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
+          if mode = Normal andalso is_none output_result then writeln else K ()
         val ctxt = Proof.context_of state
         val {facts = chained, goal, ...} = Proof.goal state
         val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -150,7 +150,7 @@
 fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
     (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
   let
-    val _ = if debug then Output.urgent_message "Constructing Isar proof..." else ()
+    val _ = if debug then writeln "Constructing Isar proof..." else ()
 
     fun generate_proof_text () =
       let
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -1016,7 +1016,7 @@
       val num_isar_deps = length isar_deps
     in
       if verbose andalso auto_level = 0 then
-        Output.urgent_message ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^
+        writeln ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^
           string_of_int num_isar_deps ^ " + " ^ string_of_int (length facts - num_isar_deps) ^
           " facts.")
       else
@@ -1025,7 +1025,7 @@
         {outcome = NONE, used_facts, ...} =>
         (if verbose andalso auto_level = 0 then
            let val num_facts = length used_facts in
-             Output.urgent_message ("Found proof with " ^ string_of_int num_facts ^ " fact" ^
+             writeln ("Found proof with " ^ string_of_int num_facts ^ " fact" ^
                plural_s num_facts ^ ".")
            end
          else
@@ -1212,7 +1212,7 @@
     |> pairself (map fact_of_raw_fact)
   end
 
-fun mash_unlearn () = (clear_state (); Output.urgent_message "Reset MaSh.")
+fun mash_unlearn () = (clear_state (); writeln "Reset MaSh.")
 
 fun learn_wrt_access_graph ctxt (name, parents, feats, deps)
     (accum as (access_G, (fact_xtab, feat_xtab))) =
@@ -1361,11 +1361,11 @@
             end
 
         fun commit last learns relearns flops =
-          (if debug andalso auto_level = 0 then Output.urgent_message "Committing..." else ();
+          (if debug andalso auto_level = 0 then writeln "Committing..." else ();
            map_state ctxt (do_commit (rev learns) relearns flops);
            if not last andalso auto_level = 0 then
              let val num_proofs = length learns + length relearns in
-               Output.urgent_message ("Learned " ^ string_of_int num_proofs ^ " " ^
+               writeln ("Learned " ^ string_of_int num_proofs ^ " " ^
                  (if run_prover then "automatic" else "Isar") ^ " proof" ^
                  plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout ^ ".")
              end
@@ -1474,18 +1474,18 @@
 
     fun learn auto_level run_prover =
       mash_learn_facts ctxt params prover auto_level run_prover one_year facts
-      |> Output.urgent_message
+      |> writeln
   in
     if run_prover then
-      (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
+      (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
          plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ " timeout: " ^
          string_of_time timeout ^ ").\n\nCollecting Isar proofs first...");
        learn 1 false;
-       Output.urgent_message "Now collecting automatic proofs. This may take several hours. You \
+       writeln "Now collecting automatic proofs. This may take several hours. You \
          \can safely stop the learning process at any point.";
        learn 0 true)
     else
-      (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
+      (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
          plural_s num_facts ^ " for Isar proofs...");
        learn 0 false)
   end
@@ -1522,7 +1522,7 @@
            Time.toSeconds timeout >= min_secs_for_learning then
           let val timeout = time_mult learn_timeout_slack timeout in
             (if verbose then
-               Output.urgent_message ("Started MaShing through " ^
+               writeln ("Started MaShing through " ^
                  (if exact then "" else "at least ") ^ string_of_int min_num_facts_to_learn ^
                  " fact" ^ plural_s min_num_facts_to_learn ^ " in the background.")
              else
@@ -1545,7 +1545,7 @@
             | num_facts_to_learn =>
               if num_facts_to_learn <= max_facts_to_learn_before_query then
                 mash_learn_facts ctxt params prover 2 false timeout facts
-                |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s))
+                |> (fn "" => () | s => writeln (MaShN ^ ": " ^ s))
               else
                 maybe_launch_thread true num_facts_to_learn)
           else
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -198,7 +198,7 @@
       sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt)
       |> List.partition (String.isPrefix remote_prefix)
   in
-    Output.urgent_message ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".")
+    writeln ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".")
   end
 
 fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -250,7 +250,7 @@
                 quote name ^ " slice #" ^ string_of_int (slice + 1) ^
                 " with " ^ string_of_int num_facts ^ " fact" ^
                 plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
-                |> Output.urgent_message
+                |> writeln
               else
                 ()
             val readable_names = not (Config.get ctxt atp_full_names)
@@ -370,7 +370,7 @@
           (used_facts, preferred_methss,
            fn preplay =>
               let
-                val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
+                val _ = if verbose then writeln "Generating proof text..." else ()
 
                 fun isar_params () =
                   let
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -76,7 +76,7 @@
     (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "")
   end
 
-fun print silent f = if silent then () else Output.urgent_message (f ())
+fun print silent f = if silent then () else writeln (f ())
 
 fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
       type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -113,7 +113,7 @@
           if debug then
             quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
             " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
-            |> Output.urgent_message
+            |> writeln
           else
             ()
         val birth = Timer.checkRealTimer timer
@@ -163,7 +163,7 @@
                 string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
                 " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
                 "..."
-                |> Output.urgent_message
+                |> writeln
               else
                 ()
           in
@@ -204,7 +204,7 @@
           (preferred_methss,
            fn preplay =>
              let
-               val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
+               val _ = if verbose then writeln "Generating proof text..." else ()
 
                fun isar_params () =
                  (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
diff -r 22b87ab47d3b -r 521cea5fa777 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -124,12 +124,12 @@
     if mode = Normal then
       "Trying " ^ space_implode " " (Try.serial_commas "and" (map (quote o fst) named_methods)) ^
       "..."
-      |> Output.urgent_message
+      |> writeln
     else
       ();
     (case par_map (fn f => f mode timeout_opt quad st) apply_methods of
       [] =>
-      (if mode = Normal then Output.urgent_message "No proof found." else (); (false, (noneN, st)))
+      (if mode = Normal then writeln "No proof found." else (); (false, (noneN, st)))
     | xs as (name, command, _) :: _ =>
       let
         val xs = xs |> map (fn (name, _, n) => (n, name))
@@ -152,7 +152,7 @@
            |> (if mode = Auto_Try then
                  Proof.goal_message (fn () => Pretty.markup Markup.information [Pretty.str message])
                else
-                 tap (fn _ => Output.urgent_message message))))
+                 tap (fn _ => writeln message))))
       end)
   end;
 
diff -r 22b87ab47d3b -r 521cea5fa777 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Pure/General/output.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -26,7 +26,6 @@
   val physical_writeln: output -> unit
   exception Protocol_Message of Properties.T
   val writelns: string list -> unit
-  val urgent_message: string -> unit
   val error_message': serial * string -> unit
   val error_message: string -> unit
   val system_message: string -> unit
@@ -42,7 +41,6 @@
 sig
   include OUTPUT
   val writeln_fn: (output list -> unit) Unsynchronized.ref
-  val urgent_message_fn: (output list -> unit) Unsynchronized.ref
   val tracing_fn: (output list -> unit) Unsynchronized.ref
   val warning_fn: (output list -> unit) Unsynchronized.ref
   val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
@@ -98,7 +96,6 @@
 exception Protocol_Message of Properties.T;
 
 val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
-val urgent_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);  (*Proof General legacy*)
 val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
 val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
 val error_message_fn =
@@ -113,7 +110,6 @@
 
 fun writelns ss = ! writeln_fn (map output ss);
 fun writeln s = writelns [s];
-fun urgent_message s = ! urgent_message_fn [output s];  (*Proof General legacy*)
 fun tracing s = ! tracing_fn [output s];
 fun warning s = ! warning_fn [output s];
 fun error_message' (i, s) = ! error_message_fn (i, [output s]);
diff -r 22b87ab47d3b -r 521cea5fa777 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Pure/Isar/calculation.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -120,7 +120,7 @@
       if int then
         Proof_Context.pretty_fact ctxt'
           (Proof_Context.full_name ctxt' (Binding.name calculationN), calc)
-        |> Pretty.string_of |> Output.urgent_message
+        |> Pretty.string_of |> writeln
       else ();
   in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
 
diff -r 22b87ab47d3b -r 521cea5fa777 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Pure/Isar/runtime.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -172,7 +172,7 @@
     (fn () =>
       debugging NONE body () handle exn =>
         if Exn.is_interrupt exn then ()
-        else Output.urgent_message ("## INTERNAL ERROR ##\n" ^ exn_message exn),
+        else writeln ("## INTERNAL ERROR ##\n" ^ exn_message exn),
       Simple_Thread.attributes interrupts);
 
 end;
diff -r 22b87ab47d3b -r 521cea5fa777 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Pure/Proof/extraction.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -121,7 +121,7 @@
 fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
 fun corr_name s vs = extr_name s vs ^ "_correctness";
 
-fun msg d s = Output.urgent_message (Pretty.spaces d ^ s);
+fun msg d s = writeln (Pretty.spaces d ^ s);
 
 fun vars_of t = map Var (rev (Term.add_vars t []));
 fun frees_of t = map Free (rev (Term.add_frees t []));
diff -r 22b87ab47d3b -r 521cea5fa777 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Pure/System/isabelle_process.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -126,7 +126,6 @@
       (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
     Output.system_message_fn := message Markup.systemN [];
     Output.protocol_message_fn := message Markup.protocolN;
-    Output.urgent_message_fn := ! Output.writeln_fn;
     Output.prompt_fn := ignore;
     message Markup.initN [] [Session.welcome ()];
     msg_channel
diff -r 22b87ab47d3b -r 521cea5fa777 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -143,7 +143,7 @@
   else
     let
       val succs = thy_graph String_Graph.all_succs [name];
-      val _ = Output.urgent_message ("Theory loader: removing " ^ commas_quote succs);
+      val _ = writeln ("Theory loader: removing " ^ commas_quote succs);
       val _ = List.app (perform Remove) succs;
       val _ = change_thys (fold String_Graph.del_node succs);
     in () end);
@@ -269,7 +269,7 @@
 fun load_thy document last_timing initiators update_time deps text (name, pos) keywords parents =
   let
     val _ = kill_thy name;
-    val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
+    val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
     val _ = Output.try_protocol_message (Markup.loading_theory name) [];
 
     val {master = (thy_path, _), imports} = deps;
@@ -405,7 +405,7 @@
   in
     NAMED_CRITICAL "Thy_Info" (fn () =>
      (kill_thy name;
-      Output.urgent_message ("Registering theory " ^ quote name);
+      writeln ("Registering theory " ^ quote name);
       update_thy (make_deps master imports) theory))
   end;
 
diff -r 22b87ab47d3b -r 521cea5fa777 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Tools/quickcheck.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -294,11 +294,11 @@
         if is_interactive then exc () else raise TimeLimit.TimeOut
   else f ();
 
-fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s;
+fun message ctxt s = if Config.get ctxt quiet then () else writeln s;
 
 fun verbose_message ctxt s =
   if not (Config.get ctxt quiet) andalso Config.get ctxt verbose
-  then Output.urgent_message s else ();
+  then writeln s else ();
 
 fun test_terms ctxt (limit_time, is_interactive) insts goals =
   (case active_testers ctxt of
@@ -517,7 +517,7 @@
   gen_quickcheck args i (Toplevel.proof_of state)
   |> apfst (Option.map (the o get_first response_of))
   |> (fn (r, state) =>
-      Output.urgent_message (Pretty.string_of
+      writeln (Pretty.string_of
         (pretty_counterex (Proof.context_of state) false r)));
 
 val parse_arg =
@@ -563,7 +563,7 @@
              |> (if auto then
                    Proof.goal_message (K (Pretty.mark Markup.information msg))
                  else
-                   tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
+                   tap (fn _ => writeln (Pretty.string_of msg))))
           else
             (noneN, state)
         end)
diff -r 22b87ab47d3b -r 521cea5fa777 src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Tools/solve_direct.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -83,13 +83,13 @@
                    Pretty.markup Markup.information (message results))
              else
                tap (fn _ =>
-                 Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
+                 writeln (Pretty.string_of (Pretty.chunks (message results))))))
     | SOME NONE =>
-        (if mode = Normal then Output.urgent_message "No proof found."
+        (if mode = Normal then writeln "No proof found."
          else ();
          (noneN, state))
     | NONE =>
-        (if mode = Normal then Output.urgent_message "An error occurred."
+        (if mode = Normal then writeln "An error occurred."
          else ();
          (unknownN, state)))
   end
diff -r 22b87ab47d3b -r 521cea5fa777 src/Tools/try.ML
--- a/src/Tools/try.ML	Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Tools/try.ML	Fri Oct 31 11:36:41 2014 +0100
@@ -60,19 +60,19 @@
 
 fun try_tools state =
   if subgoal_count state = 0 then
-    (Output.urgent_message "No subgoal!"; NONE)
+    (writeln "No subgoal!"; NONE)
   else
     get_tools (Proof.theory_of state)
     |> tap (fn tools =>
                "Trying " ^ space_implode " "
                     (serial_commas "and" (map (quote o fst) tools)) ^ "..."
-               |> Output.urgent_message)
+               |> writeln)
     |> Par_List.get_some
            (fn (name, (_, _, tool)) =>
                case try (tool false) state of
                  SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
                | _ => NONE)
-    |> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ())
+    |> tap (fn NONE => writeln "Tried in vain." | _ => ())
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "try"}