src/HOL/Auth/Event_lemmas.ML

--- a/src/HOL/Auth/Event_lemmas.ML	Fri Feb 16 08:27:17 2001 +0100
+++ b/src/HOL/Auth/Event_lemmas.ML	Fri Feb 16 13:25:08 2001 +0100
@@ -69,7 +69,7 @@
 (*Use with addSEs to derive contradictions from old Says events containing
   items known to be fresh*)
 bind_thms ("knows_Spy_partsEs", 
-           make_elim (Says_imp_knows_Spy RS parts.Inj) :: partsEs);
+           map make_elim [Says_imp_knows_Spy RS parts.Inj, parts.Body]);
 
 Addsimps [knows_Spy_Says, knows_Spy_Notes, knows_Spy_Gets];