# HG changeset patch # User paulson # Date 880559347 -3600 # Node ID 22596d62ce0b1c5d2c94b0fc9b4e751d5e8a08fb # Parent b69eedd3aa6cacd4bca2ba55364444720925feb7 updated comment diff -r b69eedd3aa6c -r 22596d62ce0b src/Provers/hypsubst.ML --- 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.