src/HOL/Tools/recdef_package.ML
changeset 19770 be5c23ebe1eb
parent 19686 83611262823e
child 20291 c82b667b6dcc
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Mon Jun 05 14:22:58 2006 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Mon Jun 05 14:26:07 2006 +0200
     1.3 @@ -300,7 +300,7 @@
     1.4    LocalRecdefData.init #>
     1.5    Attrib.add_attributes
     1.6     [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
     1.7 -    (recdef_congN, Attrib.add_del_args (FundefPackage.cong_add o cong_add) (FundefPackage.cong_del o cong_del), "declaration of recdef cong rule"),
     1.8 +    (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
     1.9      (recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")];
    1.10  
    1.11