renamed unsafe_addss to addss
authoroheimb
Fri, 16 May 1997 13:02:28 +0200
changeset 3209 ccb55f3121d1
parent 3208 8336393de482
child 3210 e80db1660614
renamed unsafe_addss to addss
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";