diff -r bc084e1b4d8d -r 351b3c2b0d83 src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Mon Mar 01 18:37:52 1999 +0100
+++ b/src/HOL/UNITY/SubstAx.ML	Mon Mar 01 18:38:43 1999 +0100
@@ -79,7 +79,7 @@
 
 val prems = 
 Goal "(!!i. i : I ==> F : LeadsTo (A i) B) ==> F : LeadsTo (UN i:I. A i) B";
-by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
+by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
 by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1);
 qed "LeadsTo_UN";
 
@@ -190,7 +190,7 @@
 val prems = 
 Goal "(!! i. i:I ==> F : LeadsTo (A i) (A' i)) \
 \     ==> F : LeadsTo (UN i:I. A i) (UN i:I. A' i)";
-by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
+by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] 
                         addIs prems) 1);
 qed "LeadsTo_UN_UN";