src/HOL/UNITY/UNITY_tactics.ML
changeset 42795 66fcc9882784
parent 42793 88bee9f6eec7
child 45138 ba618e9288b8
     1.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Fri May 13 23:24:06 2011 +0200
     1.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Fri May 13 23:58:40 2011 +0200
     1.3 @@ -59,6 +59,3 @@
     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 -Simplifier.change_simpset (fn ss => ss
     1.8 -  addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
     1.9 -  addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}));