# HG changeset patch
# User nipkow
# Date 870421298 -7200
# Node ID 5a47b869d16a44fa2650a57529d75b0d9b8f2a7f
# Parent  b87c86b6c29157c8e15f3202c80f410be1e68fc0
Had to remove {x.x=a} = a from !simpset in one proof.

diff -r b87c86b6c291 -r 5a47b869d16a src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Fri Aug 01 09:39:28 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Fri Aug 01 09:41:38 1997 +0200
@@ -524,7 +524,7 @@
 
 
 goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
-by (asm_simp_tac (!simpset addsimps [insert_def] 
+by (asm_simp_tac (!simpset addsimps [insert_def] delsimps [singleton_conv]
                            setloop (rtac analz_cong)) 1);
 qed "analz_insert_cong";