# HG changeset patch
# User haftmann
# Date 1211978930 -7200
# Node ID 215d64dc971e61b4fecc6a7b8f7ac266d9acaf45
# Parent  d21bb9f733640c12b38aa5bfc3d63e09a6cd166e
moved distinctness_limit to datatype_rep_proofs.ML

diff -r d21bb9f73364 -r 215d64dc971e src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed May 28 12:24:48 2008 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Wed May 28 14:48:50 2008 +0200
@@ -781,7 +781,7 @@
 (* setup theory *)
 
 val setup =
-  DatatypeProp.distinctness_limit_setup #>
+  DatatypeRepProofs.distinctness_limit_setup #>
   Method.add_methods tactic_emulations #>
   simproc_setup #>
   trfun_setup #>
diff -r d21bb9f73364 -r 215d64dc971e src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Wed May 28 12:24:48 2008 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Wed May 28 14:48:50 2008 +0200
@@ -7,8 +7,6 @@
 
 signature DATATYPE_PROP =
 sig
-  val distinctness_limit : int Config.T
-  val distinctness_limit_setup : theory -> theory
   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
@@ -37,10 +35,6 @@
 
 open DatatypeAux;
 
-(*the kind of distinctiveness axioms depends on number of constructors*)
-val (distinctness_limit, distinctness_limit_setup) =
-  Attrib.config_int "datatype_distinctness_limit" 7;
-
 fun indexify_names names =
   let
     fun index (x :: xs) tab =
@@ -89,8 +83,6 @@
 
           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
diff -r d21bb9f73364 -r 215d64dc971e src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed May 28 12:24:48 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed May 28 14:48:50 2008 +0200
@@ -13,6 +13,8 @@
 
 signature DATATYPE_REP_PROOFS =
 sig
+  val distinctness_limit : int Config.T
+  val distinctness_limit_setup : theory -> theory
   val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     string list -> DatatypeAux.descr list -> (string * sort) list ->
       (string * mixfix) list -> (string * mixfix) list list -> attribute
@@ -25,6 +27,10 @@
 
 open DatatypeAux;
 
+(*the kind of distinctiveness axioms depends on number of constructors*)
+val (distinctness_limit, distinctness_limit_setup) =
+  Attrib.config_int "datatype_distinctness_limit" 7;
+
 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
 
 val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
@@ -522,6 +528,7 @@
     fun prove_distinct_thms _ _ (_, []) = []
       | prove_distinct_thms lim dist_rewrites' (k, ts as _ :: _) =
           if k >= lim then [] else let
+            (*number of constructors < distinctness_limit : C_i ... ~= C_j ...*)
             fun prove [] = []
               | prove (t :: _ :: ts) =
                   let
@@ -532,11 +539,10 @@
 
     val distincts = DatatypeProp.make_distincts descr sorts;
     val distinct_thms = map2 (prove_distinct_thms
-      (Config.get_thy thy5 DatatypeProp.distinctness_limit))
-      dist_rewrites distincts;
+      (Config.get_thy thy5 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
+      if length constrs < Config.get_thy thy5 distinctness_limit
       then FewConstrs dists
       else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~
         constr_rep_thms ~~ rep_congs ~~ distinct_thms);