info: weak_case_cong;

--- 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);