| 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