--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Feb 18 12:16:27 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Feb 18 18:34:54 2013 +0100
@@ -905,7 +905,10 @@
fun do_facts _ [] = []
| do_facts parents ((fact as (_, th)) :: facts) =
(parents, fact) :: do_facts [nickname_of_thm th] facts
- in do_facts [] facts end
+ in
+ facts |> sort (crude_thm_ord o pairself snd)
+ |> do_facts []
+ end
fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub)
@@ -920,7 +923,6 @@
Time.+ (Timer.checkRealTimer timer, commit_timeout)
val {access_G, ...} = peek_state ctxt I
val is_in_access_G = is_fact_in_graph access_G snd
- val facts = facts |> sort (crude_thm_ord o pairself snd)
val no_new_facts = forall is_in_access_G facts
in
if no_new_facts andalso not run_prover then