src/HOL/Tools/Datatype/datatype_prop.ML
changeset 57983 6edc3529bb4e
parent 56254 a2dd9200854d
     1.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    val make_cases : string list -> descr list -> theory -> term list list
     1.5    val make_splits : string list -> descr list -> theory -> (term * term) list
     1.6    val make_case_combs : string list -> descr list -> theory -> string -> term list
     1.7 -  val make_weak_case_congs : string list -> descr list -> theory -> term list
     1.8 +  val make_case_cong_weaks : string list -> descr list -> theory -> term list
     1.9    val make_case_congs : string list -> descr list -> theory -> term list
    1.10    val make_nchotomys : descr list -> term list
    1.11  end;
    1.12 @@ -330,7 +330,7 @@
    1.13  
    1.14  (************************* additional rules for TFL ***************************)
    1.15  
    1.16 -fun make_weak_case_congs case_names descr thy =
    1.17 +fun make_case_cong_weaks case_names descr thy =
    1.18    let
    1.19      val case_combs = make_case_combs case_names descr thy "f";
    1.20