--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 04 12:28:42 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 04 12:52:48 2014 +0200
@@ -84,8 +84,9 @@
val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
val goal_t = Logic.list_implies (map prop_of chained @ hyp_ts, concl_t)
- fun try_methss [] = dont_know ()
- | try_methss (meths :: methss) =
+ fun try_methss [] [] = dont_know ()
+ | try_methss ress [] = (used_facts, hd (sort (play_outcome_ord o pairself snd) ress))
+ | try_methss ress (meths :: methss) =
let
fun mk_step fact_names meths =
Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
@@ -104,10 +105,10 @@
in
(used_facts', (meth, Played time'))
end
- | _ => try_methss methss)
+ | ress' => try_methss (ress' @ ress) methss)
end
in
- try_methss methss
+ try_methss [] methss
end
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Aug 04 12:28:42 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Aug 04 12:52:48 2014 +0200
@@ -179,13 +179,9 @@
(s |> s <> "" ? enclose " (" ")") ^ "."
end
-fun split_used_facts facts =
- facts
- |> List.partition (fn (_, (sc, _)) => sc = Chained)
-
fun one_line_proof_text ctxt num_chained
((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
- let val (chained, extra) = split_used_facts used_facts in
+ let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in
map fst extra
|> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
|> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "."