diff -r e650a3f6f600 -r ad4382e546fc src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Mon Nov 04 17:23:37 1996 +0100
+++ b/src/HOL/Auth/Yahalom.ML	Tue Nov 05 11:20:52 1996 +0100
@@ -118,30 +118,19 @@
 
 (*** Future keys can't be seen or used! ***)
 
-(*Nobody can have SEEN keys that will be generated in the future.
-  This has to be proved anew for each protocol description,
-  but should go by similar reasoning every time.  Hardest case is the
-  standard Fake rule.  
-      The Union over C is essential for the induction! *)
+(*Nobody can have SEEN keys that will be generated in the future. *)
 goal thy "!!evs. evs : yahalom lost ==> \
 \                length evs <= length evs' --> \
-\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
+\                Key (newK evs') ~: parts (sees lost Spy evs)";
 by (parts_induct_tac 1);
 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
                                            impOfSubs parts_insert_subset_Un,
                                            Suc_leD]
                                     addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy 
- "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
-\        ==> Key (newK evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_keys_not_seen";
+qed_spec_mp "new_keys_not_seen";
 Addsimps [new_keys_not_seen];
 
-(*Another variant: old messages must contain old keys!*)
+(*Variant: old messages must contain old keys!*)
 goal thy 
  "!!evs. [| Says A B X : set_of_list evs;  \
 \           Key (newK evt) : parts {X};    \
@@ -168,31 +157,25 @@
   ...very like new_keys_not_seen*)
 goal thy "!!evs. evs : yahalom lost ==> \
 \                length evs <= length evs' --> \
-\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
+\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
 by (parts_induct_tac 1);
-by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
 (*YM1, YM2 and YM3*)
 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
-(*Fake and YM4: these messages send unknown (X) components*)
-by (stac insert_commute 2);
-by (Simp_tac 2);
-(*YM4: the only way K could have been used is if it had been seen,
-  contradicting new_keys_not_seen*)
-by (REPEAT
-     (best_tac
-      (!claset addDs [impOfSubs analz_subset_parts,
-                      impOfSubs (analz_subset_parts RS keysFor_mono),
-                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
-                      Suc_leD]
+(*Fake and Oops: these messages send unknown (X) components*)
+by (EVERY
+    (map (fast_tac
+	  (!claset addDs [impOfSubs analz_subset_parts,
+			  impOfSubs (analz_subset_parts RS keysFor_mono),
+			  impOfSubs (parts_insert_subset_Un RS keysFor_mono),
+			  Suc_leD]
+                   addss (!simpset))) [3,1]));
+(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
+by (fast_tac
+      (!claset addSEs partsEs
+               addSDs [Says_imp_sees_Spy RS parts.Inj]
                addEs [new_keys_not_seen RSN(2,rev_notE)]
-               addss (!simpset)) 1));
-val lemma = result();
-
-goal thy 
- "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
-\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
-by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
-qed "new_keys_not_used";
+               addDs [Suc_leD]) 1);
+qed_spec_mp "new_keys_not_used";
 
 bind_thm ("new_keys_not_analzd",
           [analz_subset_parts RS keysFor_mono,
@@ -413,31 +396,22 @@
 
 goal thy "!!evs. evs : yahalom lost ==> \
 \                length evs <= length evt --> \
-\                Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
-by (etac yahalom.induct 1);
-(*auto_tac does not work here, as it performs safe_tac first*)
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
-                                     addcongs [disj_cong])));
-by (REPEAT_FIRST
-    (fast_tac (!claset addSEs partsEs
-	               addSDs  [Says_imp_sees_Spy RS parts.Inj]
-		       addDs  [impOfSubs analz_subset_parts,
-			       impOfSubs parts_insert_subset_Un, Suc_leD]
-		       addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy 
- "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
-\        ==> Nonce (newN evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_nonces_not_seen";
+\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
+by (parts_induct_tac 1);
+by (REPEAT_FIRST (fast_tac (!claset 
+                              addSEs partsEs
+                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
+                              addDs  [impOfSubs analz_subset_parts,
+                                      impOfSubs parts_insert_subset_Un,
+                                      Suc_leD]
+                              addss (!simpset))));
+qed_spec_mp "new_nonces_not_seen";
 Addsimps [new_nonces_not_seen];
 
-(*Another variant: old messages must contain old nonces!*)
+(*Variant: old messages must contain old nonces!*)
 goal thy 
- "!!evs. [| Says A B X : set_of_list evs;  \
-\           Nonce (newN evt) : parts {X};    \
+ "!!evs. [| Says A B X : set_of_list evs;      \
+\           Nonce (newN evt) : parts {X};      \
 \           evs : yahalom lost                 \
 \        |] ==> length evt < length evs";
 by (rtac ccontr 1);