# HG changeset patch
# User paulson
# Date 889624481 -3600
# Node ID 6d544b44a70e8f989b9711f58025783d3d4284ee
# Parent  6a7c70b053ccf17c0f3caec125255480a96caa64
spy_analz_tac now handles individual conjuncts properly

diff -r 6a7c70b053cc -r 6d544b44a70e src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Wed Mar 11 11:05:30 1998 +0100
+++ b/src/HOL/Auth/Message.ML	Wed Mar 11 14:54:41 1998 +0100
@@ -888,6 +888,14 @@
   but this application is no longer necessary if analz_insert_eq is used.
   Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
+
+val atomic_spy_analz_tac = SELECT_GOAL
+    (Fake_insert_simp_tac 1
+     THEN
+     IF_UNSOLVED (Blast.depth_tac
+		  (claset() addIs [analz_insertI,
+				   impOfSubs analz_subset_parts]) 4 1));
+
 fun spy_analz_tac i =
   DETERM
    (SELECT_GOAL
@@ -898,13 +906,8 @@
        (*...allowing further simplifications*)
        Simp_tac 1,
        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
-       DEPTH_SOLVE 
-         (Fake_insert_simp_tac 1
-          THEN
-          IF_UNSOLVED (Blast.depth_tac
-		       (claset() addIs [analz_insertI,
-					impOfSubs analz_subset_parts]) 4 1))
-       ]) i);
+       DEPTH_SOLVE (atomic_spy_analz_tac 1)]) i);
+
 
 (** Useful in many uniqueness proofs **)
 fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN