# HG changeset patch
# User blanchet
# Date 1361208894 -3600
# Node ID 5cbfc644c2614d5ce36bd9eaba15b1a06ba0117e
# Parent  0d5f8812856f5344ea1f069f1b455984a5b019e7
tuning

diff -r 0d5f8812856f -r 5cbfc644c261 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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