src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 27 14:56:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 27 14:56:35 2011 +0200
@@ -738,6 +738,10 @@
                   facts |> map untranslated_fact |> filter_used_facts used_facts
                         |> map snd
               in
+                (if mode = Minimize then
+                   Output.urgent_message "Preplaying proof..."
+                 else
+                   ());
                 play_one_line_proof debug preplay_timeout used_ths state subgoal
                                     metis_reconstructors
               end,