--- a/src/Provers/hypsubst.ML Wed Nov 26 16:48:11 1997 +0100
+++ b/src/Provers/hypsubst.ML Wed Nov 26 16:49:07 1997 +0100
@@ -78,7 +78,7 @@
When can we safely delete the equality?
Not if it equates two constants; consider 0=1.
Not if it resembles x=t[x], since substitution does not eliminate x.
- Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
+ Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
Not if it involves a variable free in the premises,
but we can't check for this -- hence bnd and bound_hyp_subst_tac
Prefer to eliminate Bound variables if possible.