src/HOL/Tools/Datatype/datatype_aux.ML
changeset 57983 6edc3529bb4e
parent 57884 36b5691b81a5
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4      case_name : string,
     1.5      case_rewrites : thm list,
     1.6      case_cong : thm,
     1.7 -    weak_case_cong : thm,
     1.8 +    case_cong_weak : thm,
     1.9      split : thm,
    1.10      split_asm: thm}
    1.11  end
    1.12 @@ -195,7 +195,7 @@
    1.13     case_name : string,
    1.14     case_rewrites : thm list,
    1.15     case_cong : thm,
    1.16 -   weak_case_cong : thm,
    1.17 +   case_cong_weak : thm,
    1.18     split : thm,
    1.19     split_asm: thm};
    1.20