src/HOL/Subst/Unify.ML
changeset 3209 ccb55f3121d1
parent 3192 a75558a4ed37
child 3241 91b543ab091b
     1.1 --- a/src/HOL/Subst/Unify.ML	Fri May 16 10:43:44 1997 +0200
     1.2 +++ b/src/HOL/Subst/Unify.ML	Fri May 16 13:02:28 1997 +0200
     1.3 @@ -145,7 +145,7 @@
     1.4  	      (!simpset addsimps [srange_iff, set_eq_subset]))); 
     1.5  by (ALLGOALS
     1.6      (fast_tac (!claset addEs [Var_intro RS disjE]
     1.7 -	               unsafe_addss (!simpset addsimps [srange_iff]))));
     1.8 +	               addss (!simpset addsimps [srange_iff]))));
     1.9  qed "var_elimR";
    1.10  
    1.11