# HG changeset patch
# User wenzelm
# Date 1237571210 -3600
# Node ID bcbc34cb97496e04c6dd1ba5c22c499ed90315e1
# Parent  983e8b6e4e6910784872aeb499db28b52221af5f
eliminated old Addsimps;

diff -r 983e8b6e4e69 -r bcbc34cb9749 src/HOL/UNITY/UNITY_tactics.ML
--- 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}));