src/Pure/ML/ml_pretty.ML
changeset 62784 0371c369ab1d
parent 62711 09df6a51ad3c
child 62819 d3ff367a16a0
     1.1 --- a/src/Pure/ML/ml_pretty.ML	Thu Mar 31 23:36:33 2016 +0200
     1.2 +++ b/src/Pure/ML/ml_pretty.ML	Fri Apr 01 11:45:04 2016 +0200
     1.3 @@ -13,8 +13,10 @@
     1.4    val block: pretty list -> pretty
     1.5    val str: string -> pretty
     1.6    val brk: FixedInt.int -> pretty
     1.7 -  val pair: ('a * int -> pretty) -> ('b * int -> pretty) -> ('a * 'b) * int -> pretty
     1.8 -  val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
     1.9 +  val pair: ('a * FixedInt.int -> pretty) -> ('b * FixedInt.int -> pretty) ->
    1.10 +    ('a * 'b) * FixedInt.int -> pretty
    1.11 +  val enum: string -> string -> string -> ('a * FixedInt.int -> pretty) ->
    1.12 +    'a list * FixedInt.int -> pretty
    1.13    val to_polyml: pretty -> PolyML.pretty
    1.14    val from_polyml: PolyML.pretty -> pretty
    1.15    val get_print_depth: unit -> int