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)

--- 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