--- a/src/HOL/UNITY/UNITY_tactics.ML Fri Mar 20 17:12:37 2009 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Fri Mar 20 18:46:50 2009 +0100
@@ -59,6 +59,6 @@
th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
-Addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair});
-
-Addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map});
+Simplifier.change_simpset (fn ss => ss
+ addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
+ addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}));