diff -r c8673078f915 -r 92715b528e78 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/Provers/blast.ML	Mon May 02 16:33:21 2011 +0200
@@ -1269,7 +1269,8 @@
 (*Public version with fixed depth*)
 fun depth_tac cs lim i st = timing_depth_tac (Timing.start ()) cs lim i st;
 
-val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
+val (depth_limit, setup_depth_limit) =
+  Attrib.config_int_global @{binding blast_depth_limit} (K 20);
 
 fun blast_tac cs i st =
     ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)