src/Pure/sign.ML
changeset 3886 eb0681305d3f
parent 3877 83c5310aaaab
child 3899 41a4abfa60fe
     1.1 --- a/src/Pure/sign.ML	Thu Oct 16 13:34:15 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Oct 16 13:36:04 1997 +0200
     1.3 @@ -402,12 +402,16 @@
     1.4  fun pretty_classrel sg (c1, c2) = Pretty.block
     1.5    [pretty_sort sg [c1], Pretty.str " <", Pretty.brk 1, pretty_sort sg [c2]];
     1.6  
     1.7 -fun pretty_arity sg (t, [], S) = Pretty.block
     1.8 -      [Pretty.str (t ^ " ::"), Pretty.brk 1, pretty_sort sg S]
     1.9 -  | pretty_arity sg (t, Ss, S) = Pretty.block
    1.10 -      [Pretty.str (t ^ " ::"), Pretty.brk 1,
    1.11 -        Pretty.list "(" ")" (map (pretty_sort sg) Ss),
    1.12 -        Pretty.brk 1, pretty_sort sg S];
    1.13 +fun pretty_arity sg (t, Ss, S) =
    1.14 +  let
    1.15 +    val t' = if ! long_names then t else intern_tycon sg t;
    1.16 +    val dom =
    1.17 +      if null Ss then []
    1.18 +      else [Pretty.list "(" ")" (map (pretty_sort sg) Ss), Pretty.brk 1];
    1.19 +  in
    1.20 +    Pretty.block
    1.21 +      ([Pretty.str (t ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort sg S])
    1.22 +  end;
    1.23  
    1.24  fun string_of_term sg t = Pretty.string_of (pretty_term sg t);
    1.25  fun string_of_typ sg T = Pretty.string_of (pretty_typ sg T);