# HG changeset patch
# User wenzelm
# Date 970489272 -7200
# Node ID 0f315aeee16ed66ea3e34186a0f2ce686c501bed
# Parent  20c9590bb5f5186bbc1ce4b445748ace5d38b04b
info: weak_case_cong;

diff -r 20c9590bb5f5 -r 0f315aeee16e src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Mon Oct 02 12:35:48 2000 +0200
+++ b/src/HOL/Tools/datatype_aux.ML	Mon Oct 02 14:21:12 2000 +0200
@@ -173,7 +173,8 @@
    distinct : simproc_dist,
    inject : thm list,
    nchotomy : thm,
-   case_cong : thm};
+   case_cong : thm,
+   weak_case_cong : thm};
 
 fun mk_Free s T i = Free (s ^ (string_of_int i), T);