[isabelle] "rewrite_cterm: bad background theory"



I'm experimenting with modifying theorems via attributes.
Let's say I make a function

fun my_fun ctxt thm =
  Simplifier.simplify (modify_context ctxt) thm

where modify_context adds a couple of simp rules via function
addsimps. I run the function at the ML level on an example theorem and
it does what I want.

Then I make a function

fun my_attr ctxt = Thm.rule_attribute (K (my_fun ctxt))

and set it up in Isabelle:

attribute_setup my_attr = {* Scan.succeed (my_attr @{context})*} " "

This seems to succeed, but when I run "thm some_theorem[my_attr]" I
get an exception from the raw simplifier with message "rewrite_cterm:
bad background theory". Why would this be?

Thanks.
Daniel




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