src/HOL/Integ/nat_simprocs.ML
changeset 18708 4b3dadb4fe33
parent 18442 b35d7312c64f
child 19233 77ca20b0ed77
     1.1 --- a/src/HOL/Integ/nat_simprocs.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -554,10 +554,10 @@
     1.4  in
     1.5  
     1.6  val nat_simprocs_setup =
     1.7 - [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     1.8 +  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     1.9     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    1.10      inj_thms = inj_thms, lessD = lessD, neqE = neqE,
    1.11      simpset = simpset addsimps add_rules
    1.12 -                      addsimprocs simprocs})];
    1.13 +                      addsimprocs simprocs});
    1.14  
    1.15  end;