changeset 62663 | bea354f6ff21 |
parent 62662 | 291cc01f56f5 |
child 62672 | 068b430e678f |
--- a/src/Pure/ML/ml_pretty.ML Thu Mar 17 16:56:44 2016 +0100 +++ b/src/Pure/ML/ml_pretty.ML Fri Mar 18 16:26:35 2016 +0100 @@ -114,8 +114,7 @@ (* make string *) local - fun pretty_string_of s = - "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (" ^ s ^ "))))"; + fun pretty_string_of s = "(fn x => Pretty.string_of (Pretty.from_polyml (" ^ s ^ ")))"; fun pretty_value depth = "PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ depth ^ "))"; in