[isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context
makarius at sketis.net
Thu Apr 2 20:55:16 CEST 2015
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.
More information about the isabelle-dev