src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML

         fst (fold_map rationalize_step steps subst_ctxt))
   in
     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 =
   let
     (* Make sure only type constraints inserted by the type annotation code are printed. *)

           | _ =>
             add_str (of_obtain qs (length subs) ^ " ")
             #> 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)
     and of_proof ind ctxt (Proof (xs, assms, steps)) =
       ("", ctxt)