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



Hi,

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),
  Peter


-----------------

  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 *)
  end
  
  experiment
  begin
    definition hd where "hd = 1"
  
    ML_val ‹Syntax.read_term @{context} "hd"›
    (* Fine *)
    
    term ‹\<^tag>›
    (* Inaccessible constant: "Scratch.experiment8356112.hd" *)
  end






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