# HG changeset patch
# User wenzelm
# Date 877001764 -7200
# Node ID eb0681305d3fe521894b3db36719e9552fcfe18a
# Parent  dccac762b0beaba23e644208405bf2216d9a355b
improved pretty_arity;

diff -r dccac762b0be -r eb0681305d3f src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Oct 16 13:34:15 1997 +0200
+++ b/src/Pure/sign.ML	Thu Oct 16 13:36:04 1997 +0200
@@ -402,12 +402,16 @@
 fun pretty_classrel sg (c1, c2) = Pretty.block
   [pretty_sort sg [c1], Pretty.str " <", Pretty.brk 1, pretty_sort sg [c2]];
 
-fun pretty_arity sg (t, [], S) = Pretty.block
-      [Pretty.str (t ^ " ::"), Pretty.brk 1, pretty_sort sg S]
-  | pretty_arity sg (t, Ss, S) = Pretty.block
-      [Pretty.str (t ^ " ::"), Pretty.brk 1,
-        Pretty.list "(" ")" (map (pretty_sort sg) Ss),
-        Pretty.brk 1, pretty_sort sg S];
+fun pretty_arity sg (t, Ss, S) =
+  let
+    val t' = if ! long_names then t else intern_tycon sg t;
+    val dom =
+      if null Ss then []
+      else [Pretty.list "(" ")" (map (pretty_sort sg) Ss), Pretty.brk 1];
+  in
+    Pretty.block
+      ([Pretty.str (t ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort sg S])
+  end;
 
 fun string_of_term sg t = Pretty.string_of (pretty_term sg t);
 fun string_of_typ sg T = Pretty.string_of (pretty_typ sg T);