src/Provers/blast.ML
changeset 54742 7a86358a3c0b
parent 53536 69c943125fd3
child 54897 b45b1b217f43
--- a/src/Provers/blast.ML	Fri Dec 13 23:53:02 2013 +0100
+++ b/src/Provers/blast.ML	Sat Dec 14 17:28:05 2013 +0100
@@ -1265,7 +1265,7 @@
 
 fun depth_tac ctxt lim i st =
   SELECT_GOAL
-    (Object_Logic.atomize_prems_tac 1 THEN
+    (Object_Logic.atomize_prems_tac ctxt 1 THEN
       raw_blast (Timing.start ()) ctxt lim) i st;
 
 fun blast_tac ctxt i st =
@@ -1274,7 +1274,7 @@
     val lim = Config.get ctxt depth_limit;
   in
     SELECT_GOAL
-     (Object_Logic.atomize_prems_tac 1 THEN
+     (Object_Logic.atomize_prems_tac ctxt 1 THEN
       DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1) i st
   end;