diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/General/linear_set.ML
--- 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)));