--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Thu Aug 28 16:58:27 2014 +0200
@@ -247,6 +247,7 @@
rationalize_proof ([], ctxt)
end
+val thesis_var = HOLogic.mk_Trueprop (Var ((Auto_Bind.thesisN, 0), HOLogic.boolT))
val indent_size = 2
fun string_of_isar_proof ctxt0 i n proof =
@@ -342,7 +343,7 @@
#> add_frees xs
#> add_str (" where\n" ^ of_indent (ind + 1)))
#> add_str (of_label l)
- #> add_term t
+ #> add_term (if member (op =) qs Show then thesis_var else t)
#> add_str ("\n" ^ of_indent (ind + 1) ^ of_method ls ss meth ^
(if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
and add_steps ind = fold (add_step ind)