diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Tools/find_consts.ML Wed Nov 26 20:05:34 2014 +0100 @@ -110,7 +110,7 @@ val matches = fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants [] - |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst)) + |> sort (prod_ord (rev_order o int_ord) (string_ord o apply2 fst)) |> map (apsnd fst o snd); val position_markup = Position.markup (Position.thread_data ()) Markup.position;