[isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context

Peter Lammich lammich at in.tum.de
Thu Apr 2 19:02:52 CEST 2015

> No, there is no fundamental change.  Certification is a matter of the 
> background theory of the context (the expansion of abbreviations is merely 
> a historical accident).
> The change mainly avoids awkward use of Proof_Context.theory_of in regular 
> Isabelle/ML sources -- it used to cause confusion about what the real 
> context is.  

So what is the reason not to put it in more_thm.ML? 
There, it would not affect the kernel itself, and still appear as
Thm.cterm_of to the user.


More information about the isabelle-dev mailing list