# HG changeset patch
# User oheimb
# Date 887823774 -3600
# Node ID d4a0749737152ae687a9ac68803d01fd31f9e4ce
# Parent  0a365c3e4b271d72b2f53f63182fe84cc845c5af
corrected problem with auto_tac: now uses a variant of depth_tac that avoids
interference of the simplifier with dup_step_tac

diff -r 0a365c3e4b27 -r d4a074973715 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Wed Feb 18 17:32:18 1998 +0100
+++ b/src/HOL/Auth/Shared.ML	Wed Feb 18 18:42:54 1998 +0100
@@ -179,7 +179,7 @@
 by (etac exE 1);
 by (cut_inst_tac [("evs","evs'")] 
     (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
-by Auto_tac;
+by (Asm_full_simp_tac 1 THEN depth_tac (claset()) 2 1); (* replaces Auto_tac *)
 qed "Key_supply2";
 
 goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
diff -r 0a365c3e4b27 -r d4a074973715 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Feb 18 17:32:18 1998 +0100
+++ b/src/HOL/simpdata.ML	Wed Feb 18 18:42:54 1998 +0100
@@ -476,10 +476,25 @@
 	val bdt = Blast.depth_tac cs m;
 	fun blast_depth_tac i thm = bdt i thm handle Blast.TRANS s => 
 		(warning ("Blast_tac: " ^ s); Seq.empty);
+
+	(* a variant of depth_tac that avoids interference of the simplifier 
+	   with dup_step_tac when they are combined by auto_tac *)
+	fun nodup_depth_tac cs m i state = 
+	  SELECT_GOAL 
+	   (getWrapper cs
+	    (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
+				     (safe_step_tac cs i)) THEN_ELSE
+	     (DEPTH_SOLVE (nodup_depth_tac cs m i),
+	      inst0_step_tac cs i  APPEND
+	      COND (K(m=0)) no_tac
+	        ((instp_step_tac cs i APPEND step_tac cs i)
+		 THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) i)))) 1)
+	  i state;
+
         val maintac = 
           blast_depth_tac	   (*fast but can't use addss*)
           ORELSE'
-          depth_tac cs' n;         (*slower but general*)
+          nodup_depth_tac cs' n;   (*slower but more general*)
     in  EVERY [ALLGOALS (asm_full_simp_tac ss),
 	       TRY (safe_tac cs'),
 	       REPEAT (FIRSTGOAL maintac),