src/HOL/Subst/Unify.ML

--- 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";