src/Pure/ML/ml_pretty.ML
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