# HG changeset patch
# User oheimb
# Date 909167781 -7200
# Node ID 0ad476dabbc6073870e73c0f9d09f276bf135d59
# Parent  8ef5288c24b0487a55aebb3c3349ad534944c9e1
corrected (and simplified) depth_tac

diff -r 8ef5288c24b0 -r 0ad476dabbc6 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Oct 23 20:35:56 1998 +0200
+++ b/src/Provers/classical.ML	Fri Oct 23 20:36:21 1998 +0200
@@ -108,6 +108,7 @@
   val joinrules 	: thm list * thm list -> (bool * thm) list
   val mp_tac		: int -> tactic
   val safe_tac 		: claset -> tactic
+  val safe_steps_tac 	: claset -> int -> tactic
   val safe_step_tac 	: claset -> int -> tactic
   val clarify_tac 	: claset -> int -> tactic
   val clarify_step_tac 	: claset -> int -> tactic
@@ -572,7 +573,6 @@
 fun cs addaltern   (name,    tac2) =
     cs addWrapper  (name, fn tac1 => tac1 APPEND' tac2);
 
-(*#####*)
 fun cs addD2     (name, thm) = 
     cs addaltern (name, dtac thm THEN' atac);
 fun cs addE2     (name, thm) = 
@@ -614,9 +614,12 @@
 	FIRST' hyp_subst_tacs,
 	bimatch_from_nets_tac safep_netpair]);
 
+(*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
+fun safe_steps_tac cs = REPEAT_DETERM1 o 
+	(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
+
 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
-fun safe_tac cs = REPEAT_DETERM_FIRST 
-	(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
+fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
 
 
 (*** Clarify_tac: do safe steps without causing branching ***)
@@ -716,14 +719,16 @@
   biresolve_from_nets_tac dup_netpair;
 
 (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
-fun depth_tac cs m i state = SELECT_GOAL 
-   (REPEAT_DETERM1 (COND (has_fewer_prems 1) no_tac (safe_step_tac cs 1)) 
-    THEN_ELSE (DEPTH_SOLVE (depth_tac cs m 1),
-               appWrappers cs (fn i => inst0_step_tac cs i APPEND
-	       COND (K (m=0)) no_tac
-		        ((instp_step_tac cs i APPEND dup_step_tac cs i)
-			 THEN DEPTH_SOLVE (depth_tac cs (m-1) i))) 1))
-  i state;
+local
+fun slow_step_tac' cs = appWrappers cs 
+	(instp_step_tac cs APPEND' dup_step_tac cs);
+in fun depth_tac cs m i state = SELECT_GOAL 
+   (safe_steps_tac cs 1 THEN_ELSE 
+	(DEPTH_SOLVE (depth_tac cs m 1),
+	 inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
+		(slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))
+        )) i state;
+end;
 
 (*Search, with depth bound m.  
   This is the "entry point", which does safe inferences first.*)