src/HOL/Tools/Datatype/datatype_abs_proofs.ML

   val prove_casedist_thms : config -> string list ->
     descr list -> (string * sort) list -> thm ->
     attribute list -> theory -> thm list * theory
   val prove_primrec_thms : config -> string list ->
     descr list -> (string * sort) list ->
-      (string -> thm list) -> thm list list -> thm list list ->
-        simpset -> thm -> theory -> (string list * thm list) * theory
+      (string -> thm list) -> thm list list -> thm list list * thm list list ->
+        thm -> theory -> (string list * thm list) * theory
   val prove_case_thms : config -> string list ->
     descr list -> (string * sort) list ->
       string list -> thm list -> theory -> (thm list list * string list) * theory
   val prove_split_thms : config -> string list ->
     descr list -> (string * sort) list ->

 
 
 (*************************** primrec combinators ******************************)
 
 fun prove_primrec_thms (config : config) new_type_names descr sorts
-    injects_of constr_inject dist_rewrites dist_ss induct thy =
+    injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy =
   let
     val _ = message config "Constructing primrec combinators ...";
 
     val big_name = space_implode "_" new_type_names;
     val thy0 = Sign.add_path big_name thy;

     fun mk_unique_tac ((((i, (tname, _, constrs)), elim), T), T') (tac, intrs) =
       let
         val distinct_tac =
           (if i < length newTs then
              full_simp_tac (HOL_ss addsimps (nth dist_rewrites i)) 1
-           else full_simp_tac dist_ss 1);
+           else full_simp_tac (HOL_ss addsimps (flat other_dist_rewrites)) 1);
 
         val inject = map (fn r => r RS iffD1)
           (if i < length newTs then nth constr_inject i
             else injects_of tname);