diff -r 1edc2cc25f19 -r 76d68444cd59 src/HOL/Metis_Examples/Trans_Closure.thy
--- a/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Feb 14 22:49:22 2013 +0100
@@ -44,7 +44,7 @@
 
 lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
        \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
-(* sledgehammer [isar_proofs, isar_shrink = 2] *)
+(* sledgehammer [isar_proofs, isar_compress = 2] *)
 proof -
   assume A1: "f c = Intg x"
   assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"