src/Pure/ML/ml_antiquotations.ML
changeset 62662 291cc01f56f5
parent 62240 e099a94290c1
child 62850 1f1a2c33ccf4
     1.1 --- a/src/Pure/ML/ml_antiquotations.ML	Thu Mar 17 13:44:18 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Thu Mar 17 16:56:44 2016 +0100
     1.3 @@ -21,9 +21,6 @@
     1.4    ML_Antiquotation.inline @{binding assert}
     1.5      (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
     1.6  
     1.7 -  ML_Antiquotation.inline @{binding make_string}
     1.8 -    (Args.context >> (ml_make_string o ML_Context.struct_name)) #>
     1.9 -
    1.10    ML_Antiquotation.declaration @{binding print}
    1.11      (Scan.lift (Scan.optional Args.name "Output.writeln"))
    1.12        (fn src => fn output => fn ctxt =>
    1.13 @@ -36,7 +33,8 @@
    1.14              \  (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
    1.15              ML_Syntax.print_position pos ^ "));\n";
    1.16            val body =
    1.17 -            "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ml_make_string struct_name ^ " x); x))";
    1.18 +            "(fn x => (" ^ struct_name ^ "." ^ a ^
    1.19 +              " (" ^ ML_Pretty.make_string_fn struct_name ^ " x); x))";
    1.20          in (K (env, body), ctxt') end));
    1.21  
    1.22