src/Pure/Tools/find_consts.ML
changeset 59058 a78612c67ec0
parent 58928 23d0ffd48006
child 59083 88b0b1f28adc
     1.1 --- a/src/Pure/Tools/find_consts.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -110,7 +110,7 @@
     1.4  
     1.5      val matches =
     1.6        fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants []
     1.7 -      |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
     1.8 +      |> sort (prod_ord (rev_order o int_ord) (string_ord o apply2 fst))
     1.9        |> map (apsnd fst o snd);
    1.10  
    1.11      val position_markup = Position.markup (Position.thread_data ()) Markup.position;