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

[Peter Lammich]

> 
> 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.


--
  Peter