theory Scratch
  imports Main
begin

ML \<open>
  fun mark_term (Const (c, T)) = Const (Lexicon.mark_const c, T)
    | mark_term (Free (x, T)) = Const (Lexicon.mark_fixed x, T)
    | mark_term (t $ u) = mark_term t $ mark_term u
    | mark_term (Abs (x, T, b)) = Abs (x, T, mark_term b)
    | mark_term a = a;
\<close>

syntax "_Tag" :: "logic" ("\<^tag>")

parse_translation \<open>
  [(\<^syntax_const>\<open>_Tag\<close>, fn ctxt => fn _ => 
    mark_term (Syntax.read_term ctxt "hd"))]
\<close>


definition hd where "hd = 1"

term hd  \<comment> \<open>\<open>Scratch.hd\<close>\<close>
term \<open>\<^tag>\<close>  \<comment> \<open>\<open>Scratch.hd\<close>\<close>
term \<open>\<lambda>hd. \<^tag>\<close>  \<comment> \<open>\<open>\<lambda>hda. Scratch.hd\<close>\<close>


experiment
begin
definition hd where "hd = 1"

term hd  \<comment> \<open>\<open>local.hd\<close>\<close>
term \<open>\<^tag>\<close>  \<comment> \<open>\<open>local.hd\<close>\<close>
term \<open>\<lambda>hdd. \<^tag>\<close>  \<comment> \<open>\<open>\<lambda>hda. local.hd\<close>\<close>

end

end