changeset 54897 | b45b1b217f43 |
parent 54742 | 7a86358a3c0b |
child 54942 | ed36358c20d5 |
--- a/src/Provers/blast.ML Wed Jan 01 14:32:31 2014 +0100 +++ b/src/Provers/blast.ML Wed Jan 01 20:14:47 2014 +0100 @@ -1258,7 +1258,6 @@ end in prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont) - |> Seq.maps Thm.flexflex_rule end handle PROVE => Seq.empty | TRANS s => (if Config.get ctxt trace then warning ("Blast: " ^ s) else (); Seq.empty);