# HG changeset patch
# User haftmann
# Date 1254747910 -7200
# Node ID 5281cebb1a37d2c9e00c7099581b82ebffffb589
# Parent  333945c9ac6a0e0616d730ba58f5f55c61d70282
experimental de-facto abolishment of distinctness limit

diff -r 333945c9ac6a -r 5281cebb1a37 src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- 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);