diff -r 5a5d076a9863 -r 582b655da757 src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Jun 21 16:40:55 2004 +0200
+++ b/src/Pure/display.ML	Mon Jun 21 16:41:06 2004 +0200
@@ -203,7 +203,7 @@
     fun pretty_nonterminals ts = Pretty.block
       (Pretty.breaks (Pretty.str "syntactic types:" :: map Pretty.str ts));
 
-    fun pretty_abbr (t, (vs, rhs)) = Pretty.block
+    fun pretty_abbr (t, (vs, rhs, _)) = Pretty.block
       [prt_typ_no_tvars (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
         Pretty.str " =", Pretty.brk 1, prt_typ_no_tvars rhs];