[isabelle] Attribute code called 3 times



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.