# HG changeset patch
# User oheimb
# Date 863703992 -7200
# Node ID c1653e2e146d0d800987b0cac3d38099b40b9109
# Parent  af42c8cc8e753515320518506a7b4e4166df0a23
corrected depth_tac: no call for safe_step_tac if subgoal not present

diff -r af42c8cc8e75 -r c1653e2e146d src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu May 15 15:18:00 1997 +0200
+++ b/src/Provers/classical.ML	Thu May 15 15:46:32 1997 +0200
@@ -598,7 +598,8 @@
 fun depth_tac cs m i = STATE(fn state => 
   SELECT_GOAL 
    (getWrapper cs
-    (fn i => REPEAT_DETERM1 (safe_step_tac cs i) THEN_ELSE
+    (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
+			     (safe_step_tac cs i)) THEN_ELSE
      (DEPTH_SOLVE (depth_tac cs m i),
       inst0_step_tac cs i  APPEND
       COND (K(m=0)) no_tac