diff -r f3ac344284ff -r 948e8b7ea82f src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Wed Jan 29 20:11:38 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Wed Jan 29 22:34:34 2014 +0100
@@ -122,9 +122,7 @@
     fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
 
     fun of_indent ind = replicate_string (ind * indent_size) " "
-
     fun of_moreover ind = of_indent ind ^ "moreover\n"
-
     fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
 
     fun of_obtain qs nr =
@@ -136,7 +134,6 @@
          "") ^ "obtain"
 
     fun of_show_have qs = if member (op =) qs Show then "show" else "have"
-
     fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
 
     fun of_have qs nr =