--- 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