--- a/src/HOL/Auth/NS_Public_Bad.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML Thu Dec 19 11:58:39 1996 +0100
@@ -89,9 +89,8 @@
(*** Future nonces can't be seen or used! ***)
-goal thy "!!evs. evs : ns_public ==> \
-\ length evs <= length evt --> \
-\ Nonce (newN evt) ~: parts (sees lost Spy evs)";
+goal thy "!!i. evs : ns_public ==> \
+\ length evs <= i --> Nonce (newN i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (fast_tac (!claset
addSEs partsEs
@@ -109,7 +108,7 @@
fun analz_induct_tac i =
etac ns_public.induct i THEN
ALLGOALS (asm_simp_tac
- (!simpset addsimps ([not_parts_not_analz] @ pushes)
+ (!simpset addsimps [not_parts_not_analz]
setloop split_tac [expand_if]));