Modified comment.

--- a/src/HOL/Set.ML	Thu Oct 16 15:23:53 1997 +0200
+++ b/src/HOL/Set.ML	Thu Oct 16 15:31:12 1997 +0200
@@ -601,7 +601,9 @@
 val prems = goalw thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
 by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
 qed "image_eqI";
-(* FIXME: Addsimps [image_eqI];*)
+(* Addsimps [image_eqI];
+   breaks Auth: together with shrK_neq in Shared.ML it loops.  :-(
+*)
 
 bind_thm ("imageI", refl RS image_eqI);