moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs

--- a/src/HOL/Nominal/nominal_package.ML	Fri May 23 16:05:02 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Fri May 23 16:05:04 2008 +0200
@@ -850,26 +850,22 @@
 
     (* prove distinctness theorems *)
 
-    val distinctness_limit = Config.get_thy thy8 DatatypeProp.distinctness_limit;
-    val thy8' = Config.put_thy DatatypeProp.distinctness_limit 1000 thy8;
-    val distinct_props = DatatypeProp.make_distincts new_type_names descr' sorts' thy8';
-    val thy8 = Config.put_thy DatatypeProp.distinctness_limit distinctness_limit thy8';
-
+    val distinct_props = DatatypeProp.make_distincts descr' sorts';
     val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
       dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
         (constr_rep_thmss ~~ dist_lemmas);
 
-    fun prove_distinct_thms (_, []) = []
-      | prove_distinct_thms (p as (rep_thms, dist_lemma), t::ts) =
+    fun prove_distinct_thms _ (_, []) = []
+      | prove_distinct_thms (p as (rep_thms, dist_lemma)) (k, t :: ts) =
           let
             val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
               simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
-          in dist_thm::(standard (dist_thm RS not_sym))::
-            (prove_distinct_thms (p, ts))
+          in dist_thm :: (standard (dist_thm RS not_sym)) ::
+            (prove_distinct_thms p (k, ts))
           end;
 
-    val distinct_thms = map prove_distinct_thms
-      (constr_rep_thmss ~~ dist_lemmas ~~ distinct_props);
+    val distinct_thms = map2 prove_distinct_thms
+      (constr_rep_thmss ~~ dist_lemmas) distinct_props;
 
     (** prove equations for permutation functions **)
 

--- a/src/HOL/Tools/datatype_prop.ML	Fri May 23 16:05:02 2008 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Fri May 23 16:05:04 2008 +0200
@@ -12,6 +12,8 @@
   val indexify_names: string list -> string list
   val make_tnames: typ list -> string list
   val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list
+  val make_distincts : DatatypeAux.descr list ->
+    (string * sort) list -> (int * term list) list
   val make_ind : DatatypeAux.descr list -> (string * sort) list -> term
   val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list
   val make_primrec_Ts : DatatypeAux.descr list -> (string * sort) list ->
@@ -20,8 +22,6 @@
     (string * sort) list -> theory -> term list
   val make_cases : string list -> DatatypeAux.descr list ->
     (string * sort) list -> theory -> term list list
-  val make_distincts : string list -> DatatypeAux.descr list ->
-    (string * sort) list -> theory -> term list list
   val make_splits : string list -> DatatypeAux.descr list ->
     (string * sort) list -> theory -> (term * term) list
   val make_weak_case_congs : string list -> DatatypeAux.descr list ->
@@ -59,6 +59,43 @@
   in indexify_names (map type_name Ts) end;
 
 
+(************************* distinctness of constructors ***********************)
+
+fun make_distincts descr sorts =
+  let
+    val descr' = List.concat descr;
+    val recTs = get_rec_types descr' sorts;
+    val newTs = Library.take (length (hd descr), recTs);
+
+    fun prep_constr (cname, cargs) = (cname, map (typ_of_dtyp descr' sorts) cargs);
+
+    fun make_distincts' _ [] = []
+      | make_distincts' T ((cname, cargs)::constrs) =
+          let
+            val frees = map Free ((make_tnames cargs) ~~ cargs);
+            val t = list_comb (Const (cname, cargs ---> T), frees);
+
+            fun make_distincts'' [] = []
+              | make_distincts'' ((cname', cargs')::constrs') =
+                  let
+                    val frees' = map Free ((map ((op ^) o (rpair "'"))
+                      (make_tnames cargs')) ~~ cargs');
+                    val t' = list_comb (Const (cname', cargs' ---> T), frees')
+                  in
+                    HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t')) ::
+                    HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t', t)) ::
+                      make_distincts'' constrs'
+                  end
+
+          in make_distincts'' constrs @ make_distincts' T constrs end;
+
+    (**** number of constructors < distinctness_limit : C_i ... ~= C_j ... ****)
+
+  in
+    map2 (fn ((_, (_, _, constrs))) => fn T =>
+      (length constrs, make_distincts' T (map prep_constr constrs))) (hd descr) newTs
+  end;
+
 (************************* injectivity of constructors ************************)
 
 fun make_injs descr sorts =
@@ -268,45 +305,6 @@
       ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f"))
   end;
 
-(************************* distinctness of constructors ***********************)
-
-fun make_distincts new_type_names descr sorts thy =
-  let
-    val descr' = List.concat descr;
-    val recTs = get_rec_types descr' sorts;
-    val newTs = Library.take (length (hd descr), recTs);
-
-    (**** number of constructors < distinctness_limit : C_i ... ~= C_j ... ****)
-
-    fun make_distincts_1 _ [] = []
-      | make_distincts_1 T ((cname, cargs)::constrs) =
-          let
-            val Ts = map (typ_of_dtyp descr' sorts) cargs;
-            val frees = map Free ((make_tnames Ts) ~~ Ts);
-            val t = list_comb (Const (cname, Ts ---> T), frees);
-
-            fun make_distincts' [] = []
-              | make_distincts' ((cname', cargs')::constrs') =
-                  let
-                    val Ts' = map (typ_of_dtyp descr' sorts) cargs';
-                    val frees' = map Free ((map ((op ^) o (rpair "'"))
-                      (make_tnames Ts')) ~~ Ts');
-                    val t' = list_comb (Const (cname', Ts' ---> T), frees')
-                  in
-                    (HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t')))::
-                    (HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t', t)))::
-                      (make_distincts' constrs')
-                  end
-
-          in (make_distincts' constrs) @ (make_distincts_1 T constrs)
-          end;
-
-  in map (fn (((_, (_, _, constrs)), T), tname) =>
-      if length constrs < Config.get_thy thy distinctness_limit
-      then make_distincts_1 T constrs else [])
-        ((hd descr) ~~ newTs ~~ new_type_names)
-  end;
-
 
 (*************************** the "split" - equations **************************)
 

--- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri May 23 16:05:02 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri May 23 16:05:04 2008 +0200
@@ -519,17 +519,21 @@
       dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
         (constr_rep_thms ~~ dist_lemmas);
 
-    fun prove_distinct_thms (_, []) = []
-      | prove_distinct_thms (dist_rewrites', t::_::ts) =
-          let
-            val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
-              EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
-          in dist_thm::(standard (dist_thm RS not_sym))::
-            (prove_distinct_thms (dist_rewrites', ts))
-          end;
+    fun prove_distinct_thms _ _ (_, []) = []
+      | prove_distinct_thms lim dist_rewrites' (k, ts as _ :: _) =
+          if k >= lim then [] else let
+            fun prove [] = []
+              | prove (t :: _ :: ts) =
+                  let
+                    val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
+                      EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
+                  in dist_thm :: standard (dist_thm RS not_sym) :: prove ts end;
+          in prove ts end;
 
-    val distinct_thms = map prove_distinct_thms (dist_rewrites ~~
-      DatatypeProp.make_distincts new_type_names descr sorts thy5);
+    val distincts = DatatypeProp.make_distincts descr sorts;
+    val distinct_thms = map2 (prove_distinct_thms
+      (Config.get_thy thy5 DatatypeProp.distinctness_limit))
+      dist_rewrites distincts;
 
     val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) =>
       if length constrs < Config.get_thy thy5 DatatypeProp.distinctness_limit