--- a/src/Pure/General/table.ML Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/General/table.ML Thu Sep 05 17:39:45 2024 +0200
@@ -617,12 +617,7 @@
val _ =
ML_system_pp (fn depth => fn pretty => fn tab =>
- 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 tab, depth)));
+ ML_Pretty.enum "," "{" "}" (ML_Pretty.pair ML_system_pretty pretty) (dest tab, depth));
(*final declarations of this structure!*)