src/Pure/ML/ml_antiquotation.ML
changeset 64556 851ae0e7b09c
parent 62900 c641bf9402fd
child 67146 909dcdec2122
     1.1 --- a/src/Pure/ML/ml_antiquotation.ML	Mon Dec 12 17:40:06 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_antiquotation.ML	Tue Dec 13 11:51:42 2016 +0100
     1.3 @@ -34,16 +34,16 @@
     1.4  (* basic antiquotations *)
     1.5  
     1.6  val _ = Theory.setup
     1.7 - (declaration (Binding.make ("here", @{here})) (Scan.succeed ())
     1.8 + (declaration (Binding.make ("here", \<^here>)) (Scan.succeed ())
     1.9      (fn src => fn () =>
    1.10        ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #>
    1.11  
    1.12 -  inline (Binding.make ("make_string", @{here})) (Args.context >> K ML_Pretty.make_string_fn) #>
    1.13 +  inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #>
    1.14  
    1.15 -  value (Binding.make ("binding", @{here}))
    1.16 +  value (Binding.make ("binding", \<^here>))
    1.17      (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
    1.18  
    1.19 -  value (Binding.make ("cartouche", @{here}))
    1.20 +  value (Binding.make ("cartouche", \<^here>))
    1.21      (Scan.lift Args.cartouche_input >> (fn source =>
    1.22        "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
    1.23          ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));