src/Pure/ML-Systems/polyml_common.ML
changeset 28557 6a661aeff564
parent 28488 18fea7e88ea1
child 29564 f8b933a62151
--- a/src/Pure/ML-Systems/polyml_common.ML	Thu Oct 09 21:06:08 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Thu Oct 09 21:34:05 2008 +0200
@@ -75,10 +75,6 @@
 
 (* 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);