Re: [isabelle] Attribute code called 3 times



Hi Cezary,

This effect is due to the Haftmann and Wenzel "local theory sandwich".
It's once called for the auxillary context, once for the local context, and once for the theory context.

It somewhat stores the data in three different layers.
However, when you lookup data, you will probably only see one version from the one layer you are working in.

What's the point of getting it called only once anyway?

Lukas


On 03/10/2012 11:38 PM, Cezary Kaliszyk wrote:
Hi all,

I want to define an attribute, that takes a string as an argument
with the code below:

ML {* fun attr s = let val _ = warning s in
       (Thm.rule_attribute (fn _ =>  fn y =>  y)) end *}
setup {* Attrib.setup (Binding.name "map_const")
       (Scan.lift Parse.string>>  attr) "..." *}
lemma [map_const "foo"]: True
   by simp

However upon defining the lemma, "foo" is printed 3 times. Is there a
good reason why the attribute code is called 3 times and is it
possible to get it called only once?

Regards,

Cezary







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