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