changeset 80809 | 4a64fc4d1cde |
parent 62819 | d3ff367a16a0 |
--- 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;