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

[Makarius]

On Thu, 2 Apr 2015, Peter Lammich wrote:

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

The kernel is not affected by a line like this:

   val cterm_of = global_cterm_of o Proof_Context.theory_of;

It is immediately clear what it does, and that there is no problem with 
it. This mail thread could have been shortened by posting the ML 
definition earlier. But the main thing is not the kernel here, it is user 
ML code that is a bit outdated concerning proper use of context.


 	Makarius