author | oheimb |
Fri, 16 May 1997 13:02:28 +0200 | |
changeset 3209 | ccb55f3121d1 |
parent 3208 | 8336393de482 |
child 3210 | e80db1660614 |
--- a/src/HOL/Subst/Unify.ML Fri May 16 10:43:44 1997 +0200 +++ b/src/HOL/Subst/Unify.ML Fri May 16 13:02:28 1997 +0200 @@ -145,7 +145,7 @@ (!simpset addsimps [srange_iff, set_eq_subset]))); by (ALLGOALS (fast_tac (!claset addEs [Var_intro RS disjE] - unsafe_addss (!simpset addsimps [srange_iff])))); + addss (!simpset addsimps [srange_iff])))); qed "var_elimR";