src/HOL/Auth/Shared.ML

--- a/src/HOL/Auth/Shared.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -424,5 +424,5 @@
 goal thy  
  "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
 \        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
-by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
+by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
 qed "analz_image_freshK_lemma";