--- a/src/HOL/Metis_Examples/TransClosure.thy Fri May 14 22:29:50 2010 +0200
+++ b/src/HOL/Metis_Examples/TransClosure.thy Fri May 14 22:30:24 2010 +0200
@@ -39,7 +39,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_proof, shrink_factor = 2] *)
+(* sledgehammer [isar_proof, isar_shrink_factor = 2] *)
proof -
assume A1: "f c = Intg x"
assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"