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