# HG changeset patch
# User oheimb
# Date 863780548 -7200
# Node ID ccb55f3121d14522fe498b2ccdb75d988b8306ec
# Parent  8336393de4825e29f275d5445a43a2013322f6b7
renamed unsafe_addss to addss

diff -r 8336393de482 -r ccb55f3121d1 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";