src/HOL/Tools/datatype_prop.ML

 Characteristic properties of datatypes.
 *)
 
 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
   val make_ind : DatatypeAux.descr list -> (string * sort) list -> term
   val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list

 struct
 
 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
     fun index (x :: xs) tab =
       (case AList.lookup (op =) tab x of

   let
     val descr' = List.concat descr;
     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) =
           let
             val Ts = map (typ_of_dtyp descr' sorts) cargs;

 
           in (make_distincts' constrs) @ (make_distincts_1 T constrs)
           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;
 
 
 (*************************** the "split" - equations **************************)