src/HOL/Tools/Datatype/datatype_aux.ML
changeset 57983 6edc3529bb4e
parent 57884 36b5691b81a5
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Aug 18 17:19:58 2014 +0200
@@ -27,7 +27,7 @@
     case_name : string,
     case_rewrites : thm list,
     case_cong : thm,
-    weak_case_cong : thm,
+    case_cong_weak : thm,
     split : thm,
     split_asm: thm}
 end
@@ -195,7 +195,7 @@
    case_name : string,
    case_rewrites : thm list,
    case_cong : thm,
-   weak_case_cong : thm,
+   case_cong_weak : thm,
    split : thm,
    split_asm: thm};