compile
authorblanchet
Mon Mar 28 12:11:54 2016 +0200 (2016-03-28)
changeset 62738fe827c6fa8c5
parent 62737 bdb5fd0050f5
child 62739 628c97d39627
child 62748 aa0084adce1f
compile
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/TPTP/sledgehammer_tactics.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Mar 28 12:05:47 2016 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Mar 28 12:11:54 2016 +0200
     1.3 @@ -432,7 +432,7 @@
     1.4          val prover = get_prover ctxt prover_name params goal facts
     1.5          val problem =
     1.6            {comment = "", state = st', goal = goal, subgoal = i,
     1.7 -           subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss}
     1.8 +           subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss, found_proof = I}
     1.9        in prover params problem end)) ()
    1.10        handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut
    1.11             | Fail "inappropriate" => failed ATP_Proof.Inappropriate
     2.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Mon Mar 28 12:05:47 2016 +0200
     2.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Mon Mar 28 12:11:54 2016 +0200
     2.3 @@ -45,7 +45,7 @@
     2.4        |> hd |> snd
     2.5      val problem =
     2.6        {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
     2.7 -       factss = [("", facts)]}
     2.8 +       factss = [("", facts)], found_proof = I}
     2.9    in
    2.10      (case prover params problem of
    2.11        {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME