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);