# HG changeset patch
# User blanchet
# Date 1409245357 -7200
# Node ID 32d3fa94ebb461a2087921bbd802dc81acf190b0
# Parent  f9ff405162a13106fd979f4b2576b23947ad7e1e
use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)

diff -r f9ff405162a1 -r 32d3fa94ebb4 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Aug 28 17:25:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Aug 28 19:02:37 2014 +0200
@@ -247,7 +247,13 @@
     rationalize_proof ([], ctxt)
   end
 
-val thesis_var = HOLogic.mk_Trueprop (Var ((Auto_Bind.thesisN, 0), HOLogic.boolT))
+val thesis_var = ((Auto_Bind.thesisN, 0), HOLogic.boolT)
+
+fun is_thesis ctxt t =
+  (case Vartab.lookup (Variable.binds_of ctxt) (fst thesis_var) of
+    SOME (_, t') => HOLogic.mk_Trueprop t' aconv t
+  | NONE => false)
+
 val indent_size = 2
 
 fun string_of_isar_proof ctxt0 i n proof =
@@ -343,7 +349,7 @@
             #> add_frees xs
             #> add_str (" where\n" ^ of_indent (ind + 1)))
         #> add_str (of_label l)
-        #> add_term (if member (op =) qs Show then thesis_var else t)
+        #> add_term (if is_thesis ctxt t then HOLogic.mk_Trueprop (Var 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)