src/HOL/UNITY/UNITY_tactics.ML
changeset 30610 bcbc34cb9749
parent 27239 f2f42f9fa09d
child 34234 86a985e9b4df
     1.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Fri Mar 20 17:12:37 2009 +0100
     1.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Fri Mar 20 18:46:50 2009 +0100
     1.3 @@ -59,6 +59,6 @@
     1.4       th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
     1.5       th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
     1.6  
     1.7 -Addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair});
     1.8 -
     1.9 -Addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map});
    1.10 +Simplifier.change_simpset (fn ss => ss
    1.11 +  addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
    1.12 +  addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}));