# HG changeset patch
# User blanchet
# Date 1403590762 -7200
# Node ID a9c2272d01f630994a6ea2d27a3abb9bd9de45f7
# Parent  886ff14f20cc2d78a095d68635a2054dad6e9207
don't accidentally transform 'show' into 'obtains' (in general, more 'obtain's could be turned into 'have's, but this is not necessary for the correctness of the proof)

diff -r 886ff14f20cc -r a9c2272d01f6 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Jun 22 12:37:55 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Tue Jun 24 08:19:22 2014 +0200
@@ -94,8 +94,8 @@
     val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
     val gfs = union (op =) gfs1 gfs2
   in
-    (Prove (qs2, union (op =) fix1 fix2, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths,
-       comment1 ^ comment2), hopeless)
+    (Prove (qs2, if member (op =) qs2 Show then [] else union (op =) fix1 fix2, l2, t,
+       subproofs1 @ subproofs2, (lfs, gfs), meths, comment1 ^ comment2), hopeless)
   end
 
 val merge_slack_time = seconds 0.005