src/Provers/blast.ML

--- a/src/Provers/blast.ML	Mon May 10 17:37:32 2010 +0200
+++ b/src/Provers/blast.ML	Mon May 10 20:53:06 2010 +0200
@@ -1278,7 +1278,7 @@
 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)
+    ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
         (timing_depth_tac (start_timing ()) cs) 0) i
      THEN flexflex_tac) st
     handle TRANS s =>