--- a/src/Pure/General/linear_set.ML Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/General/linear_set.ML Thu Mar 03 11:59:03 2016 +0100
@@ -137,9 +137,11 @@
val _ =
PolyML.addPrettyPrinter (fn depth => fn pretty => fn set =>
- ml_pretty
+ ML_Pretty.to_polyml
(ML_Pretty.enum "," "{" "}"
- (ML_Pretty.pair (pretty_ml o PolyML.prettyRepresentation) (pretty_ml o pretty))
+ (ML_Pretty.pair
+ (ML_Pretty.from_polyml o PolyML.prettyRepresentation)
+ (ML_Pretty.from_polyml o pretty))
(dest set, depth)));
end;