uniform use of flexflex_rule;
authorwenzelm
Fri Jun 10 12:51:29 2011 +0200 (2011-06-10)
changeset 433483e153e719039
parent 43347 f18cf88453d6
child 43349 46b4f57fb034
uniform use of flexflex_rule;
src/Provers/blast.ML
     1.1 --- a/src/Provers/blast.ML	Fri Jun 10 11:47:52 2011 +0200
     1.2 +++ b/src/Provers/blast.ML	Fri Jun 10 12:51:29 2011 +0200
     1.3 @@ -1262,6 +1262,7 @@
     1.4            end
     1.5    in
     1.6      prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont)
     1.7 +    |> Seq.maps Thm.flexflex_rule
     1.8    end
     1.9    handle PROVE => Seq.empty
    1.10      | TRANS s => (if Config.get ctxt trace then warning ("Blast: " ^ s) else (); Seq.empty);
    1.11 @@ -1271,7 +1272,6 @@
    1.12      (Object_Logic.atomize_prems_tac 1 THEN
    1.13        raw_blast (Timing.start ()) ctxt lim) i st;
    1.14  
    1.15 -
    1.16  fun blast_tac ctxt i st =
    1.17    let
    1.18      val start = Timing.start ();
    1.19 @@ -1279,8 +1279,7 @@
    1.20    in
    1.21      SELECT_GOAL
    1.22       (Object_Logic.atomize_prems_tac 1 THEN
    1.23 -      DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1 THEN
    1.24 -      flexflex_tac) i st
    1.25 +      DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1) i st
    1.26    end;
    1.27  
    1.28