--- 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