src/Pure/General/linear_set.ML

--- a/src/Pure/General/linear_set.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/General/linear_set.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -137,12 +137,7 @@
 
 val _ =
   ML_system_pp (fn depth => fn pretty => fn set =>
-    ML_Pretty.to_polyml
-      (ML_Pretty.enum "," "{" "}"
-        (ML_Pretty.pair
-          (ML_Pretty.from_polyml o ML_system_pretty)
-          (ML_Pretty.from_polyml o pretty))
-        (dest set, depth)));
+    ML_Pretty.enum "," "{" "}" (ML_Pretty.pair ML_system_pretty pretty) (dest set, depth));
 
 end;