# HG changeset patch
# User nipkow
# Date 877071796 -7200
# Node ID 4f19a40a9343bac9e4f0fa8e2ce94435defaa1bb
# Parent  51c00e87bd6edbb1350380d59d81bb3ef76eeb13
Removed image_eqI from simpset because of clash with neq_shrK.

diff -r 51c00e87bd6e -r 4f19a40a9343 src/HOL/Auth/Shared.ML
--- 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 ***)