src/Pure/General/pretty.ML
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 =