# HG changeset patch
# User blanchet
# Date 1297177809 -3600
# Node ID 1ef01508bb9ba3e536c647aaf2328fcfae00e399
# Parent  7cca2de892960596e773c1eb7fa4f87cb122c745
sort E weights

diff -r 7cca2de89296 -r 1ef01508bb9b src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Feb 08 16:10:08 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Feb 08 16:10:09 2011 +0100
@@ -681,5 +681,6 @@
   |> add_conjectures_weights (these (AList.lookup (op =) problem conjsN))
   |> add_facts_weights (these (AList.lookup (op =) problem factsN))
   |> Symtab.dest
+  |> sort (prod_ord Real.compare string_ord o pairself swap)
 
 end;