changeset 62823 | 751bcf0473a7 |
parent 62820 | 5c678ee5d34a |
child 62899 | 845ed4584e21 |
--- a/src/Pure/General/pretty.ML Sat Apr 02 22:13:00 2016 +0200 +++ b/src/Pure/General/pretty.ML Sat Apr 02 22:38:26 2016 +0200 @@ -76,8 +76,8 @@ val writeln_chunks2: T list -> unit 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 + val to_polyml: T -> PolyML_Pretty.pretty + val from_polyml: PolyML_Pretty.pretty -> T end; structure Pretty: PRETTY =