# HG changeset patch
# User wenzelm
# Date 1185909560 -7200
# Node ID f1eb34ae33af8ba996ff249eb66d9c76b8f60f02
# Parent  86734ba03ca2a43f20afeceecafb97d348630ed6
replaced dtK ref by datatype_distinctness_limit configuration option;

diff -r 86734ba03ca2 -r f1eb34ae33af src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Tue Jul 31 21:19:18 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Tue Jul 31 21:19:20 2007 +0200
@@ -880,8 +880,10 @@
 
     (* prove distinctness theorems *)
 
-    val distinct_props = setmp DatatypeProp.dtK 1000
-      (DatatypeProp.make_distincts new_type_names descr' sorts') thy8;
+    val distinctness_limit = ConfigOption.get_thy thy8 DatatypeProp.distinctness_limit;
+    val thy8' = ConfigOption.put_thy DatatypeProp.distinctness_limit 1000 thy8;
+    val distinct_props = DatatypeProp.make_distincts new_type_names descr' sorts' thy8';
+    val thy8 = ConfigOption.put_thy DatatypeProp.distinctness_limit distinctness_limit thy8';
 
     val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
       dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
diff -r 86734ba03ca2 -r f1eb34ae33af src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Tue Jul 31 21:19:18 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Tue Jul 31 21:19:20 2007 +0200
@@ -930,7 +930,10 @@
 (* setup theory *)
 
 val setup =
-  Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
+  DatatypeProp.distinctness_limit_setup #>
+  Method.add_methods tactic_emulations #>
+  simproc_setup #>
+  trfun_setup;
 
 
 (* outer syntax *)
diff -r 86734ba03ca2 -r f1eb34ae33af src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Tue Jul 31 21:19:18 2007 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Tue Jul 31 21:19:20 2007 +0200
@@ -7,7 +7,8 @@
 
 signature DATATYPE_PROP =
 sig
-  val dtK : int ref
+  val distinctness_limit : int ConfigOption.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
@@ -39,7 +40,8 @@
 open DatatypeAux;
 
 (*the kind of distinctiveness axioms depends on number of constructors*)
-val dtK = ref 7;
+val (distinctness_limit, distinctness_limit_setup) =
+  ConfigOption.int "datatype_distinctness_limit" 7;
 
 fun indexify_names names =
   let
@@ -277,7 +279,7 @@
     val recTs = get_rec_types descr' sorts;
     val newTs = Library.take (length (hd descr), recTs);
 
-    (**** number of constructors < dtK : C_i ... ~= C_j ... ****)
+    (**** number of constructors < distinctness_limit : C_i ... ~= C_j ... ****)
 
     fun make_distincts_1 _ [] = []
       | make_distincts_1 T ((cname, cargs)::constrs) =
@@ -303,7 +305,8 @@
           end;
 
   in map (fn (((_, (_, _, constrs)), T), tname) =>
-      if length constrs < !dtK then make_distincts_1 T constrs else [])
+      if length constrs < ConfigOption.get_thy thy distinctness_limit
+      then make_distincts_1 T constrs else [])
         ((hd descr) ~~ newTs ~~ new_type_names)
   end;
 
diff -r 86734ba03ca2 -r f1eb34ae33af src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 31 21:19:18 2007 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 31 21:19:20 2007 +0200
@@ -526,7 +526,8 @@
       DatatypeProp.make_distincts new_type_names descr sorts thy5);
 
     val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) =>
-      if length constrs < !DatatypeProp.dtK then FewConstrs dists
+      if length constrs < ConfigOption.get_thy thy5 DatatypeProp.distinctness_limit
+      then FewConstrs dists
       else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~
         constr_rep_thms ~~ rep_congs ~~ distinct_thms);