1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 07 19:40:56 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 07 21:28:14 2006 +0100
     1.3 @@ -27,6 +27,7 @@
     1.4      val cong_del: attribute
     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 @@ -162,17 +163,35 @@
    1.12  val cong_add = Thm.declaration_attribute (map_fundef_congs o Drule.add_rule o safe_mk_meta_eq);
    1.13  val cong_del = Thm.declaration_attribute (map_fundef_congs o Drule.del_rule o safe_mk_meta_eq);
    1.14  
    1.15 +(* Datatype hook to declare datatype congs as "fundef_congs" *)
    1.16 +
    1.17 +
    1.18 +fun add_case_cong n thy = 
    1.19 +    Context.theory_map (map_fundef_congs (Drule.add_rule 
    1.20 +                          (DatatypePackage.get_datatype thy n |> the
    1.21 +                           |> #case_cong
    1.22 +                           |> safe_mk_meta_eq))) 
    1.23 +                       thy
    1.24 +
    1.25 +val case_cong_hook = fold add_case_cong
    1.26 +
    1.27 +val setup_case_cong_hook = 
    1.28 +    DatatypeHooks.add case_cong_hook
    1.29 +    #> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy)
    1.30  
    1.31  (* setup *)
    1.32  
    1.33 -val setup = FundefData.init #> FundefCongs.init
    1.34 -        #>  Attrib.add_attributes
    1.35 -                [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
    1.36 -
    1.37 +val setup = 
    1.38 +    FundefData.init 
    1.39 +      #> FundefCongs.init
    1.40 +      #>  Attrib.add_attributes
    1.41 +            [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
    1.42 +      #> setup_case_cong_hook
    1.43  
    1.44  val get_congs = FundefCommon.get_fundef_congs o Context.Theory
    1.45  
    1.46  
    1.47 +
    1.48  (* outer syntax *)
    1.49  
    1.50  local structure P = OuterParse and K = OuterKeyword in