# HG changeset patch
# User paulson
# Date 840709621 -7200
# Node ID 4e29ea45520de2b88477fa6f8f2b0d89929628ef
# Parent  e59ff0eb1e91a6c4a14c1ed59e39f5d2cbe7670a
Now deepen_tac can take advantage of wrappers --
including addss...

diff -r e59ff0eb1e91 -r 4e29ea45520d src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Aug 22 12:24:58 1996 +0200
+++ b/src/Provers/classical.ML	Thu Aug 22 12:27:01 1996 +0200
@@ -66,6 +66,7 @@
   val best_tac 		: claset -> int -> tactic
   val slow_best_tac 	: claset -> int -> tactic
   val depth_tac		: claset -> int -> int -> tactic
+  val DEEPEN  	        : (int -> int -> tactic) -> int -> int -> tactic
   val deepen_tac	: claset -> int -> int -> tactic
 
   val contr_tac 	: int -> tactic
@@ -550,12 +551,13 @@
 (*Searching to depth m.*)
 fun depth_tac cs m i = STATE(fn state => 
   SELECT_GOAL 
+   (getwrapper cs
     (REPEAT_DETERM1 (safe_step_tac cs 1) THEN_ELSE
      (DEPTH_SOLVE (depth_tac cs m 1),
       inst0_step_tac cs 1  APPEND
       COND (K(m=0)) no_tac
         ((instp_step_tac cs 1 APPEND dup_step_tac cs 1)
-	 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))))
+	 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1)))))
   i);
 
 (*Iterative deepening tactical.  Allows us to "deepen" any search tactic*)