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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
