src/Provers/blast.ML

   handle PROVE => Seq.empty
     | TRANS s => (if Config.get ctxt trace then warning ("Blast: " ^ s) else (); Seq.empty);
 
 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 =
   let
     val start = Timing.start ();
     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;