1.1 --- a/src/Pure/Tools/find_consts.ML	Sat Mar 17 10:55:08 2012 +0100
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Sat Mar 17 11:23:14 2012 +0100
     1.3 @@ -36,11 +36,11 @@
     1.4  fun opt_not f (c as (_, (ty, _))) =
     1.5    if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
     1.6  
     1.7 -fun filter_const _ NONE = NONE
     1.8 -  | filter_const f (SOME (c, r)) =
     1.9 +fun filter_const _ _ NONE = NONE
    1.10 +  | filter_const c f (SOME rank) =
    1.11        (case f c of
    1.12          NONE => NONE
    1.13 -      | SOME i => SOME (c, Int.min (r, i)));
    1.14 +      | SOME i => SOME (Int.min (rank, i)));
    1.15  
    1.16  
    1.17  (* pretty results *)
    1.18 @@ -103,14 +103,13 @@
    1.19      val consts = Sign.consts_of thy;
    1.20      val (_, consts_tab) = #constants (Consts.dest consts);
    1.21      fun eval_entry c =
    1.22 -      fold filter_const (user_visible consts :: criteria)
    1.23 -        (SOME (c, low_ranking));
    1.24 +      fold (filter_const c) (user_visible consts :: criteria) (SOME low_ranking);
    1.25  
    1.26      val matches =
    1.27 -      Symtab.fold (cons o eval_entry) consts_tab []
    1.28 -      |> map_filter I
    1.29 -      |> sort (rev_order o int_ord o pairself snd)
    1.30 -      |> map (apsnd fst o fst);
    1.31 +      Symtab.fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c)))
    1.32 +        consts_tab []
    1.33 +      |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
    1.34 +      |> map (apsnd fst o snd);
    1.35    in
    1.36      Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
    1.37      Pretty.str "" ::