# HG changeset patch
# User paulson
# Date 880110910 -3600
# Node ID dab1833cb26dfe97b73f76dd8b04ada67b996453
# Parent  70fc6e05120c5024dbf3fecd3fb57b3ffaed012b
analz_mono_contra_tac was wrong

diff -r 70fc6e05120c -r dab1833cb26d src/HOL/Auth/Event.ML
--- a/src/HOL/Auth/Event.ML	Fri Nov 21 12:14:47 1997 +0100
+++ b/src/HOL/Auth/Event.ML	Fri Nov 21 12:15:10 1997 +0100
@@ -129,10 +129,10 @@
   this information isn't needed, the proof will be much shorter, since
   it will omit complicated reasoning about analz.*)
 val analz_mono_contra_tac = 
-  let val impI' = read_instantiate_sg (sign_of thy)
-                [("P", "?Y ~: analz (sees ?A ?evs)")] impI;
+  let val analz_impI = read_instantiate_sg (sign_of thy)
+                [("P", "?Y ~: analz (spies ?evs)")] impI;
   in
-    rtac impI THEN' 
+    rtac analz_impI THEN' 
     REPEAT1 o 
       (dresolve_tac 
        [spies_subset_spies_Says  RS analz_mono RS contra_subsetD,