--- a/src/Pure/General/pretty.ML Fri Jun 18 20:10:52 2004 +0200
+++ b/src/Pure/General/pretty.ML Sun Jun 20 09:26:29 2004 +0200
@@ -54,8 +54,7 @@
val setmargin: int -> unit
val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
type pp
- val pp: (term -> T) -> (typ -> T) -> (sort -> T) ->
- (class list -> T) -> (arity -> T) -> pp
+ val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
val pp_undef: pp
val term: pp -> term -> T
val typ: pp -> typ -> T
@@ -279,7 +278,7 @@
datatype pp =
PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
-fun pp f1 f2 f3 f4 f5 = PP (f1, f2, f3, f4, f5);
+val pp = PP;
fun pp_fun f (PP x) = f x;
@@ -297,6 +296,6 @@
fun undef kind _ = str ("*** UNABLE TO PRINT " ^ kind ^ " ***");
val pp_undef =
- pp (undef "term") (undef "typ") (undef "sort") (undef "classrel") (undef "arity");
+ pp (undef "term", undef "typ", undef "sort", undef "classrel", undef "arity");
end;