Re: [isabelle] antiquotations



On Fri, 7 Mar 2008, Jeremy Dawson wrote:

> But now I find that using @{theory} instead of the_context () produces an
> error
> 
> Exception-
>   ERROR
>      "Stale theory encountered:\n{ProtoPure, Pur (etc)
> 
> When I change this back to the_context () the error goes away.
> 
> What is a stale theory, and why does @{theory} produce a stale theory?

As explained in the Isar Implementation Manual, theory acts like a linear 
type.  The "Stale theory" error indicates that it has been used in 
non-linerar fashion.

Note that @{theory} is rarely used in production code, only in one-liner 
tests within a toplevel ML command etc.  If you really need to keep a live 
reference to a (potentially evolving) theory, then use @{theory_ref}.

Normally one would just pass through a Proof.context, instead of 
manipulating with low-level theory certificates.


	Makarius






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