# HG changeset patch
# User nipkow
# Date 877008672 -7200
# Node ID 4bbfbb7a2cd3ff716251d99d1d246d49853d9934
# Parent  c0d56e4c823e0acad97d268df58d6fa886e86083
Modified comment.

diff -r c0d56e4c823e -r 4bbfbb7a2cd3 src/HOL/Set.ML
--- 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);