--- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Jul 31 21:19:18 2007 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Jul 31 21:19:20 2007 +0200
@@ -526,7 +526,8 @@
DatatypeProp.make_distincts new_type_names descr sorts thy5);
val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) =>
- if length constrs < !DatatypeProp.dtK then FewConstrs dists
+ if length constrs < ConfigOption.get_thy thy5 DatatypeProp.distinctness_limit
+ then FewConstrs dists
else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~
constr_rep_thms ~~ rep_congs ~~ distinct_thms);