diff -r f66ab8a4e98f -r e10b0d5fa33a src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Jun 20 22:14:03 2005 +0200
+++ b/src/Pure/display.ML	Mon Jun 20 22:14:04 2005 +0200
@@ -261,7 +261,7 @@
   | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
   | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
 
-fun sort_idxs vs = map (apsnd (sort (prod_ord String.compare Int.compare))) vs;
+fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
 fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
 
 fun consts_of t = sort_cnsts (add_consts (t, []));