src/HOL/Auth/Message.ML
changeset 3583 5a47b869d16a
parent 3519 ab0a9fbed4c0
child 3650 282ffdc91884
--- 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";