diff -r bf7d82193a2e -r 8d12ac6a3e1c src/Pure/display.ML
--- a/src/Pure/display.ML	Fri Jun 20 21:00:25 2008 +0200
+++ b/src/Pure/display.ML	Fri Jun 20 21:00:26 2008 +0200
@@ -149,14 +149,14 @@
       [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
 
     val tfrees = map (fn v => TFree (v, []));
-    fun pretty_type syn (t, (Type.LogicalType n, _)) =
+    fun pretty_type syn (t, ((Type.LogicalType n, _), _)) =
           if syn then NONE
           else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
-      | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
+      | pretty_type syn (t, ((Type.Abbreviation (vs, U, syn'), _), _)) =
           if syn <> syn' then NONE
           else SOME (Pretty.block
             [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
-      | pretty_type syn (t, (Type.Nonterminal, _)) =
+      | pretty_type syn (t, ((Type.Nonterminal, _), _)) =
           if not syn then NONE
           else SOME (prt_typ (Type (t, [])));