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,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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