[isabelle] Inaccessible constant when trying to parse term from cartouche in experiment


I'm trying to parse a term that I read from a cartouche, which is
contained in another term. For that, I Syntax.read_term the content of
the cartouche inside a parse_translation. However, inside an experiment
environment, this will yield "inaccessible constant" errors. What is
going wrong here?
I attached a boiled-down example, with my test-cases. The last test-
case fails.

Thanks in advance for any help or hints (being completely lost here),


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

  parse_translation ‹
    [(@{syntax_const "_Tag"}, fn ctxt => fn _ => 
      Syntax.read_term ctxt "hd"

  (* In my real example, the "hd" is a string parsed from 
    a cartouche argument. I have to interpret this string as a term 
    in the context where the outer 
    term, containing the cartouche, appears.

  term ‹\<^tag>›
  (* Fine *)
  locale foo begin
    definition hd where "hd = 1"
    term ‹\<^tag>›
    (* Fine *)
    definition hd where "hd = 1"
    ML_val ‹Syntax.read_term @{context} "hd"›
    (* Fine *)
    term ‹\<^tag>›
    (* Inaccessible constant: "Scratch.experiment8356112.hd" *)

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.