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