src/HOL/Tools/datatype_package.ML
changeset 24098 f1eb34ae33af
parent 22994 02440636214f
child 24218 fbf1646b267c
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jul 31 21:19:18 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jul 31 21:19:20 2007 +0200
     1.3 @@ -930,7 +930,10 @@
     1.4  (* setup theory *)
     1.5  
     1.6  val setup =
     1.7 -  Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
     1.8 +  DatatypeProp.distinctness_limit_setup #>
     1.9 +  Method.add_methods tactic_emulations #>
    1.10 +  simproc_setup #>
    1.11 +  trfun_setup;
    1.12  
    1.13  
    1.14  (* outer syntax *)