src/HOL/ex/Set_Algebras.thy

--- a/src/HOL/ex/Set_Algebras.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/ex/Set_Algebras.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -321,7 +321,7 @@
 
 lemma set_plus_image:
   fixes S T :: "'n::semigroup_add set" shows "S \<oplus> T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
-  unfolding set_plus_def by (fastsimp simp: image_iff)
+  unfolding set_plus_def by (fastforce simp: image_iff)
 
 lemma set_setsum_alt:
   assumes fin: "finite I"