# HG changeset patch
# User webertj
# Date 1093793799 -7200
# Node ID 670ab849781826503b341fd74140133140354c80
# Parent  065ce5385a0696c930f656ef6bc87f69c13e8ee1
depth limit (previously hard-coded with a value of 20) made a reference

diff -r 065ce5385a06 -r 670ab8497818 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Thu Aug 26 17:28:57 2004 +0200
+++ b/src/Provers/blast.ML	Sun Aug 29 17:36:39 2004 +0200
@@ -80,6 +80,7 @@
     | $  of term*term;
   type branch
   val depth_tac 	: claset -> int -> int -> tactic
+  val depth_limit : int ref
   val blast_tac 	: claset -> int -> tactic
   val Blast_tac 	: int -> tactic
   val setup		: (theory -> theory) list
@@ -1283,8 +1284,10 @@
 (*Public version with fixed depth*)
 fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st;
 
+val depth_limit = ref 20;
+
 fun blast_tac cs i st = 
-    ((DEEPEN (1,20) (timing_depth_tac (startTiming()) cs) 0) i 
+    ((DEEPEN (1, !depth_limit) (timing_depth_tac (startTiming()) cs) 0) i 
      THEN flexflex_tac) st
     handle TRANS s =>
       ((if !trace then warning ("blast: " ^ s) else ());