src/HOL/Set.ML

--- a/src/HOL/Set.ML	Fri Oct 17 09:03:16 1997 +0200
+++ b/src/HOL/Set.ML	Fri Oct 17 09:04:02 1997 +0200
@@ -601,9 +601,7 @@
 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";
-(* Addsimps [image_eqI];
-   breaks Auth: together with shrK_neq in Shared.ML it loops.  :-(
-*)
+Addsimps [image_eqI];
 
 bind_thm ("imageI", refl RS image_eqI);