--- a/src/Pure/ML-Systems/polyml_common.ML Mon Sep 29 21:26:46 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML Mon Sep 29 21:26:49 2008 +0200
@@ -73,6 +73,10 @@
(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
+type ('a, 'b) pp =
+ (string -> unit) * (int * bool -> unit) * (int * int -> unit) * (unit -> unit) ->
+ int -> ('a * int -> unit) -> 'b -> unit;
+
fun make_pp _ pprint (str, blk, brk, en) _ _ obj =
pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
fn () => brk (99999, 0), en);