[isabelle] Parsing abbreviations in a local context



Dear Isabelle list,

After I add an abbreviation to a local context, the parser seems to ignore
it.
Is there a way to get parsing without prefixes working for abbreviations in
my local context?

Minimal example of this strange behavior:

theory t imports HOL begin
local_setup {* fn lthy =>
  let
    val lthy2 = Specification.abbreviation Syntax.mode_default
      NONE [] @{term "asd == True"} true lthy
    val _ = tracing (@{make_string} (Syntax.read_term lthy2 "asd")
  in lthy2 end
*}

Displays "Free asd" rather than "Const True".

Surprisingly, I get "Const True" if I prefix it by the theory
name (as in "t.asd") or if I reset the context, as in:
    val lthy3 = Proof_Context.init_global (Proof_Context.theory_of lthy2)
both of which I believe I should not be doing myself, so how can I get
parsing for abbreviations to work in a local context?

Regards,
Cezary

-- 
Cezary Kaliszyk, University of Innsbruck,
http://cl-informatik.uibk.ac.at/cek/



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