*** 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. The actual change is rather minor, but it required several days to go through old (and some new) applications that still did not work with the proof context correctly, e.g. see https://isabelle-dev.sketis.net/rISABELLE8ee3d5d3c1 for HOL-Nominal or https://isabelle-dev.sketis.net/rAFPe1f8faf5261f for AFP/Simpl. The new setup will prevent such inaccurate treatment of contexts in the future, because it fails rather quickly on bad situations --- with a proper error instead of just a warning from > 15 years ago https://isabelle-dev.sketis.net/rISABELLE7df8abe926c3 Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
