# HG changeset patch
# User paulson
# Date 921058960 -3600
# Node ID e53457213857fdfa16e3f2dd81528ec57436471d
# Parent  b1dec44d001845e4bb990ddb6023a2dc6286fc89
updated not_bad_tac for the Gets model

diff -r b1dec44d0018 -r e53457213857 src/HOL/Auth/Shared.ML
--- 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)