diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/General/bitset.ML --- 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!*)