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