# HG changeset patch
# User paulson
# Date 878732849 -3600
# Node ID 31251763848dc12f831bbe1c76581ed72cb0ffdd
# Parent  53f60f51333ca38256c90840d89ae3b1184bd328
Tidied Key_supply3

diff -r 53f60f51333c -r 31251763848d src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Wed Nov 05 13:26:19 1997 +0100
+++ b/src/HOL/Auth/Shared.ML	Wed Nov 05 13:27:29 1997 +0100
@@ -175,14 +175,13 @@
 \                      Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
 by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
 by (etac exE 1);
-by (cut_inst_tac [("evs","evs'")] 
+(*Blast_tac requires instantiation of the keys for some reason*)
+by (cut_inst_tac [("evs","evs'"), ("a1","K")] 
     (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
 by (etac exE 1);
-by (cut_inst_tac [("evs","evs''")] 
+by (cut_inst_tac [("evs","evs''"), ("a1","Ka"), ("a2","K")] 
     (Finites.emptyI RS Finites.insertI RS Finites.insertI RS Key_supply_ax) 1);
-by (Clarify_tac 1);
-by (Full_simp_tac 1);
-by (fast_tac (claset() addSEs [allE]) 1);
+by (Blast_tac 1);
 qed "Key_supply3";
 
 goal thy "Key (@ K. Key K ~: used evs) ~: used evs";