Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reintroduced crucial sorting accidentally lost in 962190eab40d
authorblanchet
Tue, 19 Feb 2013 13:37:07 +0100
changeset 51184 e2569dde59c8
parent 51183 e0493414ce03
child 51185 145d76c35f8b
reintroduced crucial sorting accidentally lost in 962190eab40d
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML file | annotate | diff | comparison | revisions 
--- 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))
isabelle