unparse_arity: unparse type constructor as well;
authorwenzelm
Mon Oct 15 21:08:37 2007 +0200 (2007-10-15)
changeset 2504332ed65dc1bf4
parent 25042 a33b78d63114
child 25044 de1f50ab668d
unparse_arity: unparse type constructor as well;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Mon Oct 15 21:08:36 2007 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Oct 15 21:08:37 2007 +0200
     1.3 @@ -784,10 +784,11 @@
     1.4  
     1.5  fun unparse_arity ctxt (a, Ss, S) =
     1.6    let
     1.7 +    val prtT = unparse_typ ctxt (Type (a, []));
     1.8      val dom =
     1.9        if null Ss then []
    1.10        else [Pretty.list "(" ")" (map (unparse_sort ctxt) Ss), Pretty.brk 1];
    1.11 -  in Pretty.block ([Pretty.str (a ^ " ::"), Pretty.brk 1] @ dom @ [unparse_sort ctxt S]) end;
    1.12 +  in Pretty.block ([prtT, Pretty.str " ::", Pretty.brk 1] @ dom @ [unparse_sort ctxt S]) end;
    1.13  
    1.14  
    1.15  (* read = parse + check *)