# HG changeset patch
# User wenzelm
# Date 1459503904 -7200
# Node ID 0371c369ab1de7206d1a14fddf55c190bc21769c
# Parent  75ee05386b9038071eb96e3ead70db2c530a9d19
adapted to Poly/ML repository version 2e40cadc975a;

diff -r 75ee05386b90 -r 0371c369ab1d src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu Mar 31 23:36:33 2016 +0200
+++ b/src/Pure/General/pretty.ML	Fri Apr 01 11:45:04 2016 +0200
@@ -74,7 +74,7 @@
   val block_enclose: T * T -> T list -> T
   val writeln_chunks: T list -> unit
   val writeln_chunks2: T list -> unit
-  val to_ML: int -> T -> ML_Pretty.pretty
+  val to_ML: FixedInt.int -> T -> ML_Pretty.pretty
   val from_ML: ML_Pretty.pretty -> T
   val to_polyml: T -> PolyML.pretty
   val from_polyml: PolyML.pretty -> T
diff -r 75ee05386b90 -r 0371c369ab1d src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Thu Mar 31 23:36:33 2016 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Fri Apr 01 11:45:04 2016 +0200
@@ -13,8 +13,10 @@
   val block: pretty list -> pretty
   val str: string -> pretty
   val brk: FixedInt.int -> pretty
-  val pair: ('a * int -> pretty) -> ('b * int -> pretty) -> ('a * 'b) * int -> pretty
-  val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
+  val pair: ('a * FixedInt.int -> pretty) -> ('b * FixedInt.int -> pretty) ->
+    ('a * 'b) * FixedInt.int -> pretty
+  val enum: string -> string -> string -> ('a * FixedInt.int -> pretty) ->
+    'a list * FixedInt.int -> pretty
   val to_polyml: pretty -> PolyML.pretty
   val from_polyml: PolyML.pretty -> pretty
   val get_print_depth: unit -> int