updated not_bad_tac for the Gets model

--- a/src/HOL/Auth/Shared.ML	Wed Mar 10 10:42:11 1999 +0100
+++ b/src/HOL/Auth/Shared.ML	Wed Mar 10 10:42:40 1999 +0100
@@ -63,7 +63,8 @@
 fun not_bad_tac s =
     case_tac ("(" ^ s ^ ") : bad") THEN'
     SELECT_GOAL 
-      (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
+      (REPEAT_DETERM (etac exE 1) THEN
+       REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
        REPEAT_DETERM (etac MPair_analz 1) THEN
        THEN_BEST_FIRST 
          (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)