--- a/src/Pure/General/linear_set.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/General/linear_set.ML Sat Apr 02 21:10:07 2016 +0200
@@ -136,11 +136,11 @@
(* ML pretty-printing *)
val _ =
- PolyML.addPrettyPrinter (fn depth => fn pretty => fn set =>
+ ML_system_pp (fn depth => fn pretty => fn set =>
ML_Pretty.to_polyml
(ML_Pretty.enum "," "{" "}"
(ML_Pretty.pair
- (ML_Pretty.from_polyml o PolyML.prettyRepresentation)
+ (ML_Pretty.from_polyml o ML_system_pretty)
(ML_Pretty.from_polyml o pretty))
(dest set, depth)));