diff -r 71c27b320610 -r 5d0ecd0c8f3c src/HOL/NatBin.thy --- a/src/HOL/NatBin.thy Tue Jul 31 19:40:23 2007 +0200 +++ b/src/HOL/NatBin.thy Tue Jul 31 19:40:24 2007 +0200 @@ -656,7 +656,7 @@ val numeral_ss = simpset() addsimps numerals; val nat_bin_arith_setup = - Fast_Arith.map_data + LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,