1.1 --- a/src/Provers/blast.ML	Thu Aug 26 17:28:57 2004 +0200
     1.2 +++ b/src/Provers/blast.ML	Sun Aug 29 17:36:39 2004 +0200
     1.3 @@ -80,6 +80,7 @@
     1.4      | $  of term*term;
     1.5    type branch
     1.6    val depth_tac 	: claset -> int -> int -> tactic
     1.7 +  val depth_limit : int ref
     1.8    val blast_tac 	: claset -> int -> tactic
     1.9    val Blast_tac 	: int -> tactic
    1.10    val setup		: (theory -> theory) list
    1.11 @@ -1283,8 +1284,10 @@
    1.12  (*Public version with fixed depth*)
    1.13  fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st;
    1.14  
    1.15 +val depth_limit = ref 20;
    1.16 +
    1.17  fun blast_tac cs i st = 
    1.18 -    ((DEEPEN (1,20) (timing_depth_tac (startTiming()) cs) 0) i 
    1.19 +    ((DEEPEN (1, !depth_limit) (timing_depth_tac (startTiming()) cs) 0) i 
    1.20       THEN flexflex_tac) st
    1.21      handle TRANS s =>
    1.22        ((if !trace then warning ("blast: " ^ s) else ());