More robust (and more strict) treatment of abstractions within the context

#### ML

- Term operations under abstractions are now more robust (and more strict) by using the formal proof context in subsequent operations:
`Variable.dest_abs``Variable.dest_abs_cterm``Variable.dest_all``Variable.dest_all_cterm`

This works under the assumption that terms are always properly declared to the proof context (e.g. via`Variable.declare_term`). Failure to do so, or working with the wrong context, will cause an error (exception`Fail`, based on`Term.USED_FREE`from`Term.dest_abs_fresh`).

The Simplifier and equational conversions now use the above operations routinely, and thus require user-space tools to be serious about the proof context (notably in their use of`Goal.prove`,`SUBPROOF`etc.). INCOMPATIBILITY in add-on tools is to be expected occasionally: a proper context discipline needs to be followed.

- Former operations
`Term.dest_abs`and`Logic.dest_all`(without a proper context) have been discontinued. INCOMPATIBILITY, either use`Variable.dest_abs`etc. above, or the following operations that imitate the old behavior to a great extent:`Term.dest_abs_global``Logic.dest_all_global`

This works under the assumption that the given (sub-)term directly shows all free variables that need to be avoided when generating a fresh name. A violation of the assumption are variables stemming from the enclosing context that get involved in a proof only later.

This refers to Isabelle/7f06e317fe25 + AFP/0cfcfc7a85ea.

- Projects
*None*- Subscribers
*None*