src/HOL/Tools/datatype_package.ML

        split_thms : (thm * thm) list,
        induction : thm,
        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
   val datatype_info_sg_err : Sign.sg -> string -> DatatypeAux.datatype_info
   val datatype_info_err : theory -> string -> DatatypeAux.datatype_info
   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;
 
 structure DatatypePackage : DATATYPE_PACKAGE =
 struct

 
 fun case_const_of thy tname = (case datatype_info thy tname of
    Some {case_name, ...} => Some (Const (case_name, the (Sign.const_type
      (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;
   in case assoc (frees @ params, var) of

 
 
 (**** 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 ********************)
 
 fun add_and_get_axioms_atts label tnames attss ts thy =

       (DatatypeProp.make_weak_case_congs new_type_names descr sorts thy10) thy10;
 
     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;
 
     val thy12 = thy11 |>

     val (thy11, size_thms) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
       descr sorts reccomb_names rec_thms thy10;
 
     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;
 
     val thy12 = thy11 |>
       Theory.add_path (space_implode "_" new_type_names) |>

       (#1 o store_thmss "distinct" new_type_names distinct) |>
       Theory.add_path (space_implode "_" new_type_names) |>
       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;
 
     val thy11 = thy10 |>
       (#1 o PureThy.add_thmss [(("simps", simps), []),