src/Pure/General/bitset.ML
changeset 80809 4a64fc4d1cde
parent 79080 2c457c4cd486
--- a/src/Pure/General/bitset.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/General/bitset.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -215,8 +215,7 @@
 
 val _ =
   ML_system_pp (fn depth => fn _ => fn set =>
-    ML_Pretty.to_polyml
-      (ML_Pretty.enum "," "{" "}" (ML_Pretty.from_polyml o ML_system_pretty) (dest set, depth)));
+    ML_Pretty.enum "," "{" "}" ML_system_pretty (dest set, depth));
 
 
 (*final declarations of this structure!*)