diff -r 8857237c3a90 -r 19afb533028e src/Pure/General/linear_set.ML
--- 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;