src/HOL/Tools/function_package/fundef_package.ML
changeset 24039 273698405054
parent 23819 2040846d1bbe
child 24168 86a03a092062
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sun Jul 29 14:29:52 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sun Jul 29 14:29:54 2007 +0200
     1.3 @@ -172,14 +172,14 @@
     1.4  
     1.5  (* congruence rules *)
     1.6  
     1.7 -val cong_add = Thm.declaration_attribute (map_fundef_congs o Drule.add_rule o safe_mk_meta_eq);
     1.8 -val cong_del = Thm.declaration_attribute (map_fundef_congs o Drule.del_rule o safe_mk_meta_eq);
     1.9 +val cong_add = Thm.declaration_attribute (map_fundef_congs o Thm.add_thm o safe_mk_meta_eq);
    1.10 +val cong_del = Thm.declaration_attribute (map_fundef_congs o Thm.del_thm o safe_mk_meta_eq);
    1.11  
    1.12  (* Datatype hook to declare datatype congs as "fundef_congs" *)
    1.13  
    1.14  
    1.15  fun add_case_cong n thy =
    1.16 -    Context.theory_map (map_fundef_congs (Drule.add_rule
    1.17 +    Context.theory_map (map_fundef_congs (Thm.add_thm
    1.18                            (DatatypePackage.get_datatype thy n |> the
    1.19                             |> #case_cong
    1.20                             |> safe_mk_meta_eq)))