changeset 51007 | 4f694d52bf62 |
parent 51005 | ce4290c33d73 |
child 51010 | afd0213a3dab |
--- a/src/HOL/TPTP/sledgehammer_tactics.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Thu Jan 31 17:54:05 2013 +0100 @@ -45,7 +45,7 @@ |> #1 val problem = {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, - facts = facts} + fact_triple = (facts, facts, facts)} in (case prover params (K (K (K ""))) problem of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME