changeset 43045 | c46107e6714b |
parent 42812 | dda4aef7cba4 |
child 43331 | 01f051619eee |
--- a/src/Provers/blast.ML Fri May 27 10:41:09 2011 +0200 +++ b/src/Provers/blast.ML Mon May 30 12:15:17 2011 +0100 @@ -1267,7 +1267,7 @@ prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont) |> Seq.map (rotate_prems (1 - i)) end - handle PROVE => Seq.empty; + handle PROVE => Seq.empty | THM _ => Seq.empty; (*Public version with fixed depth*) fun depth_tac ctxt lim i st = timing_depth_tac (Timing.start ()) ctxt lim i st;