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