# HG changeset patch
# User blanchet
# Date 1409237907 -7200
# Node ID 6842fb6365695eb4a1e180b4c53fbf3ccd17a909
# Parent  aa239fee063a9f6c4b3e12b8d8afa0b695923bb8
generate 'thesis' variable in Sledgehammer Isar proofs

diff -r aa239fee063a -r 6842fb636569 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- 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)