diff -r bff9c05fe229 -r f76ad0771f67 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Mon Aug 23 12:06:47 2010 +0200
+++ b/src/Pure/General/table.ML	Mon Aug 23 15:11:41 2010 +0200
@@ -392,6 +392,16 @@
 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;