1.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Oct 05 15:04:45 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Oct 05 15:05:10 2009 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5  (*the kind of distinctiveness axioms depends on number of constructors*)
     1.6  val (distinctness_limit, distinctness_limit_setup) =
     1.7 -  Attrib.config_int "datatype_distinctness_limit" 7;
     1.8 +  Attrib.config_int "datatype_distinctness_limit" 9999 (*approx. infinity*);
     1.9  
    1.10  val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
    1.11