src/HOL/Tools/datatype_package.ML
changeset 24098 f1eb34ae33af
parent 22994 02440636214f
child 24218 fbf1646b267c
--- a/src/HOL/Tools/datatype_package.ML	Tue Jul 31 21:19:18 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Tue Jul 31 21:19:20 2007 +0200
@@ -930,7 +930,10 @@
 (* setup theory *)
 
 val setup =
-  Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
+  DatatypeProp.distinctness_limit_setup #>
+  Method.add_methods tactic_emulations #>
+  simproc_setup #>
+  trfun_setup;
 
 
 (* outer syntax *)