# HG changeset patch
# User paulson
# Date 849180532 -3600
# Node ID 820f68aec6ee15a922a8d947e925946b09d3feb6
# Parent  79a2f085a7fddf6b5241754e8f706a03fec2b238
Extra fix needed in newN case

diff -r 79a2f085a7fd -r 820f68aec6ee src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Thu Nov 28 12:09:33 1996 +0100
+++ b/src/HOL/Auth/Yahalom.ML	Thu Nov 28 12:28:52 1996 +0100
@@ -402,7 +402,8 @@
 by (REPEAT_FIRST (fast_tac (!claset 
                               addSEs partsEs
                               addSDs  [Says_imp_sees_Spy RS parts.Inj]
-                              addDs  [impOfSubs analz_subset_parts,
+                              addEs  [leD RS notE]
+			      addDs  [impOfSubs analz_subset_parts,
                                       impOfSubs parts_insert_subset_Un,
                                       Suc_leD]
                               addss (!simpset))));