# HG changeset patch
# User blanchet
# Date 1361277427 -3600
# Node ID e2569dde59c8be6b66caba5c8456d1bbca03e96b
# Parent  e0493414ce03102a2e7dcf318d1afd9595f61610
reintroduced crucial sorting accidentally lost in 962190eab40d

diff -r e0493414ce03 -r e2569dde59c8 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Feb 19 13:27:33 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Feb 19 13:37:07 2013 +0100
@@ -1055,7 +1055,8 @@
           else
             let
               val new_facts =
-                facts |> attach_parents_to_facts []
+                facts |> sort (crude_thm_ord o pairself snd)
+                      |> attach_parents_to_facts []
                       |> filter_out (is_in_access_G o snd)
               val (learns, (n, _, _)) =
                 ([], (0, next_commit_time (), false))