# HG changeset patch
# User haftmann
# Date 1255415799 -7200
# Node ID a7a97960054be14bfb5661916121ba452df99eb8
# Parent  9fd51a25bd3a5c11e8a8191ae7924f559469e803
more appropriate abstraction over distinctness rules

diff -r 9fd51a25bd3a -r a7a97960054b src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Mon Oct 12 15:26:50 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Oct 13 08:36:39 2009 +0200
@@ -334,15 +334,13 @@
     val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
     val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
 
-    val other_distincts = all_distincts thy2 (get_rec_types flat_descr sorts);
-
     val (exhaust, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names
       descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
     val (nchotomys, thy4) = DatatypeAbsProofs.prove_nchotomys config new_type_names
       descr sorts exhaust thy3;
     val ((rec_names, rec_rewrites), thy5) = DatatypeAbsProofs.prove_primrec_thms
       config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
-      inject distinct (Simplifier.theory_context thy4 (HOL_basic_ss addsimps (flat other_distincts)))
+      inject (distinct, all_distincts thy2 (get_rec_types flat_descr sorts))
       induct thy4;
     val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
       config new_type_names descr sorts rec_names rec_rewrites thy5;
diff -r 9fd51a25bd3a -r a7a97960054b src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Oct 12 15:26:50 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Oct 13 08:36:39 2009 +0200
@@ -20,8 +20,8 @@
     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
@@ -88,7 +88,7 @@
 (*************************** 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 ...";
 
@@ -170,7 +170,7 @@
         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