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