src/HOL/Tools/function_package/fundef_package.ML
changeset 24626 85eceef2edc7
parent 24624 b8383b1bbae3
child 24711 e8bba7723858
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 18 07:36:38 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 18 07:46:00 2007 +0200
     1.3 @@ -26,7 +26,6 @@
     1.4      val setup_termination_proof : string option -> local_theory -> Proof.state
     1.5  
     1.6      val setup : theory -> theory
     1.7 -    val setup_case_cong_hook : theory -> theory
     1.8      val get_congs : theory -> thm list
     1.9  end
    1.10  
    1.11 @@ -176,11 +175,10 @@
    1.12                             |> safe_mk_meta_eq)))
    1.13                         thy
    1.14  
    1.15 -val case_cong_hook = fold add_case_cong
    1.16 +val case_cong = fold add_case_cong
    1.17  
    1.18 -val setup_case_cong_hook =
    1.19 -    DatatypeHooks.add case_cong_hook
    1.20 -    #> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy)
    1.21 +val setup_case_cong = DatatypePackage.add_interpretator case_cong
    1.22 +
    1.23  
    1.24  
    1.25  (* ad-hoc method to convert elimination-style goals to existential statements *)
    1.26 @@ -259,7 +257,7 @@
    1.27    Attrib.add_attributes
    1.28      [("fundef_cong", Attrib.add_del_args FundefCtxTree.cong_add FundefCtxTree.cong_del,
    1.29        "declaration of congruence rule for function definitions")]
    1.30 -  #> setup_case_cong_hook
    1.31 +  #> setup_case_cong
    1.32    #> FundefRelation.setup
    1.33    #> elim_to_cases_setup
    1.34