# HG changeset patch
# User wenzelm
# Date 1087828866 -7200
# Node ID 582b655da757da0f0314ef102f07689cdc5c00fa
# Parent  5a5d076a98638ec76cb80c615c016840fdd41e88
pretty_abbr;

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];