src/HOL/Tools/datatype_prop.ML
changeset 27002 215d64dc971e
parent 26969 cf3f998d0631
child 27300 4cb3101d2bf7
--- 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