--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Wed Dec 18 16:50:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Wed Dec 18 16:50:14 2013 +0100
@@ -238,7 +238,7 @@
#> add_suffix " = "
#> add_term t2
#> add_suffix "\n"
- | add_step ind (step as Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) =
+ | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) =
add_step_pre ind qs subproofs
#> (case xs of
[] => add_suffix (of_have qs (length subproofs) ^ " ")