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