diff -r 01b03a124b81 -r 398d7d6bba42 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Apr 27 17:20:29 2011 +0200
+++ b/src/Pure/General/name_space.ML	Wed Apr 27 17:44:06 2011 +0200
@@ -16,6 +16,7 @@
   val kind_of: T -> string
   val the_entry: T -> string ->
     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
+  val entry_ord: T -> string * string -> order
   val markup: T -> string -> Markup.T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
@@ -125,6 +126,8 @@
     NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
   | SOME (_, entry) => entry);
 
+fun entry_ord space = int_ord o pairself (#id o the_entry space);
+
 fun markup (Name_Space {kind, entries, ...}) name =
   (case Symtab.lookup entries name of
     NONE => Markup.malformed