--- a/src/HOL/Auth/Shared.ML Thu Oct 16 16:54:31 1997 +0200
+++ b/src/HOL/Auth/Shared.ML Fri Oct 17 09:03:16 1997 +0200
@@ -87,7 +87,7 @@
qed "shrK_neq";
Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
-
+Delsimps [image_eqI]; (* loops together with shrK_neq *)
(*** Fresh nonces ***)