# HG changeset patch
# User paulson
# Date 872160989 -7200
# Node ID 282ffdc918844b494c201f9341f3e17563ddd6ee
# Parent  e530286d48475fdfc32c2a0da679cd64648a7474
Replacing impOfSubs analz_mono by analz_insertI should improve convergence
of spy_analz_tac

diff -r e530286d4847 -r 282ffdc91884 src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Thu Aug 21 12:55:10 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Thu Aug 21 12:56:29 1997 +0200
@@ -884,7 +884,7 @@
          (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1
           THEN
           IF_UNSOLVED (Blast.depth_tac
-		       (!claset addIs [impOfSubs analz_mono,
+		       (!claset addIs [analz_insertI,
 				       impOfSubs analz_subset_parts]) 2 1))
        ]) i);