[isabelle-dev] Safe approach to hypothesis substitution

[Makarius]

On Wed, 25 Aug 2010, Thomas Sewell wrote:

> Finally, the change to inspect_pair is indeed just a bugfix. I don't 
> this check is needed for the simplifier driven version of hyp_subst 
> anyway, so the bug shouldn't often be seen.

Often it is hard to tell what is a bug or an obscure feature required like 
that by some other tool.

Anyway, I recommend to try that tiny bit of the change on all existing 
Isabelle + AFP theories.  Then we can apply it independently, with a more 
informative log message that "fixed bug", though.


 	Makarius