src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -604,7 +604,7 @@
 	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
 	  with AbB have "finite ?D" by simp
 	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z"
-	    using finite_imp_foldSet by rules
+	    using finite_imp_foldSet by iprover
 	  moreover have cinB: "c \<in> B" using B by auto
 	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z"
 	    by(rule Diff1_foldSet)