src/Pure/ML/ml_antiquotation.ML
changeset 62662 291cc01f56f5
parent 59112 e670969f34df
child 62850 1f1a2c33ccf4
     1.1 --- a/src/Pure/ML/ml_antiquotation.ML	Thu Mar 17 13:44:18 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_antiquotation.ML	Thu Mar 17 16:56:44 2016 +0100
     1.3 @@ -38,8 +38,10 @@
     1.4      (fn src => fn () =>
     1.5        ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #>
     1.6  
     1.7 +  inline (Binding.make ("make_string", @{here}))
     1.8 +    (Args.context >> (ML_Pretty.make_string_fn o ML_Context.struct_name)) #>
     1.9 +
    1.10    value (Binding.make ("binding", @{here}))
    1.11      (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding));
    1.12  
    1.13  end;
    1.14 -