changeset 50876 | e6317e8b11db |
parent 50866 | e12ebcb859a7 |
child 50904 | 3d2d62d29302 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Jan 14 09:59:50 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Jan 14 10:32:33 2013 +0100 @@ -209,7 +209,7 @@ mash_learn_proof ctxt params prover (prop_of goal) all_facts val launch = launch_prover params mode minimize_command only learn in - if mode = Auto_Try orelse mode = Try then + if mode = Auto_Try then (unknownN, state) |> fold (fn prover => fn accum as (outcome_code, _) => if outcome_code = someN then accum