src/Provers/blast.ML
changeset 36001 992839c4be90
parent 35625 9c818cab0dd0
child 36787 f60e4dd6d76f
--- a/src/Provers/blast.ML	Sun Mar 28 16:13:29 2010 +0200
+++ b/src/Provers/blast.ML	Sun Mar 28 16:59:06 2010 +0200
@@ -1275,7 +1275,7 @@
 (*Public version with fixed depth*)
 fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
 
-val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" 20;
+val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
 
 fun blast_tac cs i st =
     ((DEEPEN (1, Config.get_thy (Thm.theory_of_thm st) depth_limit)