# HG changeset patch
# User blanchet
# Date 1459159914 -7200
# Node ID fe827c6fa8c51de6fdf92de572414942667b1c64
# Parent  bdb5fd0050f510ca1a2f51267656e4536ff8ddd2
compile

diff -r bdb5fd0050f5 -r fe827c6fa8c5 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Mar 28 12:11:54 2016 +0200
@@ -432,7 +432,7 @@
         val prover = get_prover ctxt prover_name params goal facts
         val problem =
           {comment = "", state = st', goal = goal, subgoal = i,
-           subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss}
+           subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss, found_proof = I}
       in prover params problem end)) ()
       handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut
            | Fail "inappropriate" => failed ATP_Proof.Inappropriate
diff -r bdb5fd0050f5 -r fe827c6fa8c5 src/HOL/TPTP/sledgehammer_tactics.ML
--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Mon Mar 28 12:11:54 2016 +0200
@@ -45,7 +45,7 @@
       |> hd |> snd
     val problem =
       {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
-       factss = [("", facts)]}
+       factss = [("", facts)], found_proof = I}
   in
     (case prover params problem of
       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME