# HG changeset patch
# User blanchet
# Date 1270110405 -7200
# Node ID 3fc077c4780a67d33495d089d5bcb1ee2dce1107
# Parent  48aec67c284f7235801c320869a35d0a84649341
fixed layout of Sledgehammer output

diff -r 48aec67c284f -r 3fc077c4780a src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 29 19:49:57 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 01 10:26:45 2010 +0200
@@ -548,10 +548,10 @@
   Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" 
 fun minimize_line _ [] = ""
   | minimize_line name xs =
-      "To minimize the number of lemmas, try this command:\n" ^
+      "To minimize the number of lemmas, try this command: " ^
       Markup.markup Markup.sendback
                     ("sledgehammer minimize [atps = " ^ name ^ "] (" ^
-                     space_implode " " xs ^ ")") ^ "."
+                     space_implode " " xs ^ ")") ^ ".\n"
 
 fun metis_lemma_list dfg name (result as (_, _, _, _, goal, i)) =
   let