| changeset 36162 | 0bd034a80a9a |
| parent 33543 | a4dbf0f92d96 |
| child 38470 | 484e483eb606 |
--- a/src/Pure/ML-Systems/polyml.ML Fri Apr 16 10:15:00 2010 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Fri Apr 16 10:52:10 2010 +0200 @@ -66,3 +66,6 @@ use_text context (1, "pp") false ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); +val ml_make_string = + "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))"; +