corrected depth_tac: no call for safe_step_tac if subgoal not present

--- 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