1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed May 28 12:24:48 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed May 28 14:48:50 2008 +0200
     1.3 @@ -781,7 +781,7 @@
     1.4  (* setup theory *)
     1.5  
     1.6  val setup =
     1.7 -  DatatypeProp.distinctness_limit_setup #>
     1.8 +  DatatypeRepProofs.distinctness_limit_setup #>
     1.9    Method.add_methods tactic_emulations #>
    1.10    simproc_setup #>
    1.11    trfun_setup #>

     2.1 --- a/src/HOL/Tools/datatype_prop.ML	Wed May 28 12:24:48 2008 +0200
     2.2 +++ b/src/HOL/Tools/datatype_prop.ML	Wed May 28 14:48:50 2008 +0200
     2.3 @@ -7,8 +7,6 @@
     2.4  
     2.5  signature DATATYPE_PROP =
     2.6  sig
     2.7 -  val distinctness_limit : int Config.T
     2.8 -  val distinctness_limit_setup : theory -> theory
     2.9    val indexify_names: string list -> string list
    2.10    val make_tnames: typ list -> string list
    2.11    val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list
    2.12 @@ -37,10 +35,6 @@
    2.13  
    2.14  open DatatypeAux;
    2.15  
    2.16 -(*the kind of distinctiveness axioms depends on number of constructors*)
    2.17 -val (distinctness_limit, distinctness_limit_setup) =
    2.18 -  Attrib.config_int "datatype_distinctness_limit" 7;
    2.19 -
    2.20  fun indexify_names names =
    2.21    let
    2.22      fun index (x :: xs) tab =
    2.23 @@ -89,8 +83,6 @@
    2.24  
    2.25            in make_distincts'' constrs @ make_distincts' T constrs end;
    2.26  
    2.27 -    (**** number of constructors < distinctness_limit : C_i ... ~= C_j ... ****)
    2.28 -
    2.29    in
    2.30      map2 (fn ((_, (_, _, constrs))) => fn T =>
    2.31        (length constrs, make_distincts' T (map prep_constr constrs))) (hd descr) newTs

     3.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed May 28 12:24:48 2008 +0200
     3.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed May 28 14:48:50 2008 +0200
     3.3 @@ -13,6 +13,8 @@
     3.4  
     3.5  signature DATATYPE_REP_PROOFS =
     3.6  sig
     3.7 +  val distinctness_limit : int Config.T
     3.8 +  val distinctness_limit_setup : theory -> theory
     3.9    val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
    3.10      string list -> DatatypeAux.descr list -> (string * sort) list ->
    3.11        (string * mixfix) list -> (string * mixfix) list list -> attribute
    3.12 @@ -25,6 +27,10 @@
    3.13  
    3.14  open DatatypeAux;
    3.15  
    3.16 +(*the kind of distinctiveness axioms depends on number of constructors*)
    3.17 +val (distinctness_limit, distinctness_limit_setup) =
    3.18 +  Attrib.config_int "datatype_distinctness_limit" 7;
    3.19 +
    3.20  val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
    3.21  
    3.22  val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
    3.23 @@ -522,6 +528,7 @@
    3.24      fun prove_distinct_thms _ _ (_, []) = []
    3.25        | prove_distinct_thms lim dist_rewrites' (k, ts as _ :: _) =
    3.26            if k >= lim then [] else let
    3.27 +            (*number of constructors < distinctness_limit : C_i ... ~= C_j ...*)
    3.28              fun prove [] = []
    3.29                | prove (t :: _ :: ts) =
    3.30                    let
    3.31 @@ -532,11 +539,10 @@
    3.32  
    3.33      val distincts = DatatypeProp.make_distincts descr sorts;
    3.34      val distinct_thms = map2 (prove_distinct_thms
    3.35 -      (Config.get_thy thy5 DatatypeProp.distinctness_limit))
    3.36 -      dist_rewrites distincts;
    3.37 +      (Config.get_thy thy5 distinctness_limit)) dist_rewrites distincts;
    3.38  
    3.39      val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) =>
    3.40 -      if length constrs < Config.get_thy thy5 DatatypeProp.distinctness_limit
    3.41 +      if length constrs < Config.get_thy thy5 distinctness_limit
    3.42        then FewConstrs dists
    3.43        else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~
    3.44          constr_rep_thms ~~ rep_congs ~~ distinct_thms);