src/Pure/General/name_space.ML
changeset 60924 610794dff23c
parent 60284 014b86186c49
child 62241 a4a1f282bcd5
--- a/src/Pure/General/name_space.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/General/name_space.ML	Thu Aug 13 11:05:19 2015 +0200
@@ -602,7 +602,7 @@
   fold (fn (name, x) =>
     (verbose orelse not (is_concealed space name)) ?
       cons ((name, extern ctxt space name), x)) entries []
-  |> Library.sort_wrt (#2 o #1);
+  |> sort_by (#2 o #1);
 
 fun markup_entries verbose ctxt space entries =
   extern_entries verbose ctxt space entries