src/HOL/Tools/function_package/fundef_package.ML
changeset 24168 86a03a092062
parent 24039 273698405054
child 24508 c8b82fec6447
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Aug 07 10:03:25 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Aug 07 14:49:58 2007 +0200
     1.3 @@ -25,9 +25,6 @@
     1.4  
     1.5      val setup_termination_proof : string option -> local_theory -> Proof.state
     1.6  
     1.7 -    val cong_add: attribute
     1.8 -    val cong_del: attribute
     1.9 -
    1.10      val setup : theory -> theory
    1.11      val setup_case_cong_hook : theory -> theory
    1.12      val get_congs : theory -> thm list
    1.13 @@ -169,17 +166,11 @@
    1.14  val add_fundef_i = gen_add_fundef Specification.cert_specification
    1.15  
    1.16  
    1.17 -
    1.18 -(* congruence rules *)
    1.19 -
    1.20 -val cong_add = Thm.declaration_attribute (map_fundef_congs o Thm.add_thm o safe_mk_meta_eq);
    1.21 -val cong_del = Thm.declaration_attribute (map_fundef_congs o Thm.del_thm o safe_mk_meta_eq);
    1.22 -
    1.23  (* Datatype hook to declare datatype congs as "fundef_congs" *)
    1.24  
    1.25  
    1.26  fun add_case_cong n thy =
    1.27 -    Context.theory_map (map_fundef_congs (Thm.add_thm
    1.28 +    Context.theory_map (FundefCtxTree.map_fundef_congs (Thm.add_thm
    1.29                            (DatatypePackage.get_datatype thy n |> the
    1.30                             |> #case_cong
    1.31                             |> safe_mk_meta_eq)))
    1.32 @@ -266,14 +257,13 @@
    1.33  
    1.34  val setup =
    1.35    Attrib.add_attributes
    1.36 -    [("fundef_cong", Attrib.add_del_args cong_add cong_del,
    1.37 +    [("fundef_cong", Attrib.add_del_args FundefCtxTree.cong_add FundefCtxTree.cong_del,
    1.38        "declaration of congruence rule for function definitions")]
    1.39    #> setup_case_cong_hook
    1.40    #> FundefRelation.setup
    1.41    #> elim_to_cases_setup
    1.42  
    1.43 -val get_congs = FundefCommon.get_fundef_congs o Context.Theory
    1.44 -
    1.45 +val get_congs = FundefCtxTree.get_fundef_congs o Context.Theory
    1.46  
    1.47  
    1.48  (* outer syntax *)