export get_datatypes_sg;
added weak_case_congs_of(_sg);

--- a/src/HOL/Tools/datatype_package.ML	Mon Oct 02 14:21:12 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Mon Oct 02 14:22:39 2000 +0200
@@ -63,6 +63,7 @@
        size : thm list,
        simps : thm list}
   val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
+  val get_datatypes_sg : Sign.sg -> DatatypeAux.datatype_info Symtab.table
   val print_datatypes : theory -> unit
   val datatype_info_sg : Sign.sg -> string -> DatatypeAux.datatype_info option
   val datatype_info : theory -> string -> DatatypeAux.datatype_info option
@@ -71,6 +72,8 @@
   val constrs_of : theory -> string -> term list option
   val constrs_of_sg : Sign.sg -> string -> term list option
   val case_const_of : theory -> string -> term option
+  val weak_case_congs_of : theory -> thm list
+  val weak_case_congs_of_sg : Sign.sg -> thm list
   val setup: (theory -> theory) list
 end;
 
@@ -134,6 +137,9 @@
      (Theory.sign_of thy) case_name)))
  | _ => None);
 
+val weak_case_congs_of_sg = map (#weak_case_cong o #2) o Symtab.dest o get_datatypes_sg;
+val weak_case_congs_of = weak_case_congs_of_sg o Theory.sign_of;
+
 fun find_tname var Bi =
   let val frees = map dest_Free (term_frees Bi)
       val params = Logic.strip_params Bi;
@@ -379,20 +385,22 @@
 (**** make datatype info ****)
 
 fun make_dt_info descr induct reccomb_names rec_thms
-  ((((((((i, (_, (tname, _, _))), case_name), case_thms),
-    exhaustion_thm), distinct_thm), inject), nchotomy), case_cong) = (tname,
-      {index = i,
-       descr = descr,
-       rec_names = reccomb_names,
-       rec_rewrites = rec_thms,
-       case_name = case_name,
-       case_rewrites = case_thms,
-       induction = induct,
-       exhaustion = exhaustion_thm,
-       distinct = distinct_thm,
-       inject = inject,
-       nchotomy = nchotomy,
-       case_cong = case_cong});
+    (((((((((i, (_, (tname, _, _))), case_name), case_thms),
+      exhaustion_thm), distinct_thm), inject), nchotomy), case_cong), weak_case_cong) =
+  (tname,
+   {index = i,
+    descr = descr,
+    rec_names = reccomb_names,
+    rec_rewrites = rec_thms,
+    case_name = case_name,
+    case_rewrites = case_thms,
+    induction = induct,
+    exhaustion = exhaustion_thm,
+    distinct = distinct_thm,
+    inject = inject,
+    nchotomy = nchotomy,
+    case_cong = case_cong,
+    weak_case_cong = weak_case_cong});
 
 
 (********************* axiomatic introduction of datatypes ********************)
@@ -554,7 +562,7 @@
     val dt_infos = map (make_dt_info descr' induct reccomb_names' rec_thms)
       ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
         exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~
-          nchotomys ~~ case_congs);
+          nchotomys ~~ case_congs ~~ weak_case_congs);
 
     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
     val split_thms = split ~~ split_asm;
@@ -613,7 +621,7 @@
 
     val dt_infos = map (make_dt_info (flat descr) induct reccomb_names rec_thms)
       ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
-        casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs);
+        casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
 
     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
 
@@ -719,8 +727,8 @@
       PureThy.add_thms [(("induct", induction), [case_names_induct])];
 
     val dt_infos = map (make_dt_info descr induction' reccomb_names rec_thms)
-      ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~
-        casedist_thms ~~ map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs);
+      ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
+        map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
 
     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;