src/Pure/General/table.ML

 fun make_list args = fold_rev cons_list args empty;
 fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab);
 fun merge_list eq = join (fn _ => Library.merge eq);
 
 
+(* ML pretty-printing -- requires Poly/ML 5.3.0 or later *)
+
+val _ =
+  PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab =>
+    ml_pretty
+      (ML_Pretty.enum "," "{" "}"
+        (ML_Pretty.pair (pretty_ml o PolyML.prettyRepresentation) (pretty_ml o pretty))
+        (dest tab, depth)));
+
+
 (*final declarations of this structure!*)
 fun map f = map_table (K f);
 val map' = map_table;
 val fold = fold_table;
 val fold_rev = fold_rev_table;