Re: [isabelle] "rewrite_cterm: bad background theory"

Hi Daniel,

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

@{context} injects the *static* context, i. e. the context at the
position you are writing your declaration.  But here you need the
*dynamic* context, e.g. via something like

> attribute_setup my_attr = {* Scan.peek (my_attr o Context.proof_of) *}

Note that static contexts are rather seldom appropriate, mostly for
experimenting.  The system is built in a way that the appropriate
dynamic contexts is provided for nearly all crucial slots as a
functional argument.

AFAIR the Isabelle implementation manual provided more detail (I did not
take a look quite now).

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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