src/HOL/Tools/datatype_package.ML
changeset 26496 49ae9456eba9
parent 26343 0dd2eab7b296
child 26533 aeef55a3d1d5
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Mar 29 19:24:57 2008 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Mar 29 22:55:49 2008 +0100
     1.3 @@ -428,7 +428,7 @@
     1.4  
     1.5  val simproc_setup =
     1.6    Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t) #>
     1.7 -  (fn thy => ((change_simpset_of thy) (fn ss => ss addsimprocs [distinct_simproc]); thy));
     1.8 +  Simplifier.map_simpset (fn ss => ss addsimprocs [distinct_simproc]);
     1.9  
    1.10  
    1.11  (**** translation rules for case ****)