src/Pure/Isar/generic_target.ML
changeset 60924 610794dff23c
parent 60642 48dd1cefb4ae
child 61261 ddb2da7cb2e4
--- a/src/Pure/Isar/generic_target.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Aug 13 11:05:19 2015 +0200
@@ -102,7 +102,7 @@
    (if Context_Position.is_visible ctxt then
       warning
         ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
-          commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
+          commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^
           (if mx = NoSyn then ""
            else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)))
     else (); NoSyn);