# HG changeset patch
# User wenzelm
# Date 1331979794 -3600
# Node ID ef4b0d6b2fb61ec7900bb5d227e86f0576d161f8
# Parent  23a59a495934f11558c284af9fad5103e3a0e193
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
tuned;

diff -r 23a59a495934 -r ef4b0d6b2fb6 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Sat Mar 17 10:55:08 2012 +0100
+++ b/src/Pure/Tools/find_consts.ML	Sat Mar 17 11:23:14 2012 +0100
@@ -36,11 +36,11 @@
 fun opt_not f (c as (_, (ty, _))) =
   if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
 
-fun filter_const _ NONE = NONE
-  | filter_const f (SOME (c, r)) =
+fun filter_const _ _ NONE = NONE
+  | filter_const c f (SOME rank) =
       (case f c of
         NONE => NONE
-      | SOME i => SOME (c, Int.min (r, i)));
+      | SOME i => SOME (Int.min (rank, i)));
 
 
 (* pretty results *)
@@ -103,14 +103,13 @@
     val consts = Sign.consts_of thy;
     val (_, consts_tab) = #constants (Consts.dest consts);
     fun eval_entry c =
-      fold filter_const (user_visible consts :: criteria)
-        (SOME (c, low_ranking));
+      fold (filter_const c) (user_visible consts :: criteria) (SOME low_ranking);
 
     val matches =
-      Symtab.fold (cons o eval_entry) consts_tab []
-      |> map_filter I
-      |> sort (rev_order o int_ord o pairself snd)
-      |> map (apsnd fst o fst);
+      Symtab.fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c)))
+        consts_tab []
+      |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
+      |> map (apsnd fst o snd);
   in
     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
     Pretty.str "" ::