1.1 --- a/src/HOL/Integ/int_arith1.ML	Mon Oct 17 19:19:29 2005 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Mon Oct 17 23:10:10 2005 +0200
     1.3 @@ -309,7 +309,7 @@
     1.4    | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
     1.5  
     1.6  fun simplify_meta_eq rules ss =
     1.7 -    simplify (Simplifier.inherit_bounds ss HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
     1.8 +    simplify (Simplifier.inherit_context ss HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
     1.9      o mk_meta_eq;
    1.10  
    1.11  structure CancelNumeralsCommon =
    1.12 @@ -321,14 +321,14 @@
    1.13    val find_first_coeff  = find_first_coeff []
    1.14    val trans_tac         = fn _ => trans_tac
    1.15    fun norm_tac ss =
    1.16 -    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
    1.17 +    let val num_ss' = Simplifier.inherit_context ss num_ss in
    1.18        ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    1.19                                           diff_simps @ minus_simps @ add_ac))
    1.20        THEN ALLGOALS (simp_tac (num_ss' addsimps non_add_bin_simps @ mult_minus_simps))
    1.21        THEN ALLGOALS (simp_tac (num_ss' addsimps minus_from_mult_simps @ add_ac @ mult_ac))
    1.22      end
    1.23    fun numeral_simp_tac ss =
    1.24 -    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
    1.25 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
    1.26    val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
    1.27    end;
    1.28  
    1.29 @@ -399,14 +399,14 @@
    1.30    val prove_conv        = Bin_Simprocs.prove_conv_nohyps
    1.31    val trans_tac         = fn _ => trans_tac
    1.32    fun norm_tac ss =
    1.33 -    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
    1.34 +    let val num_ss' = Simplifier.inherit_context ss num_ss in
    1.35        ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    1.36                                            diff_simps @ minus_simps @ add_ac))
    1.37        THEN ALLGOALS (simp_tac (num_ss' addsimps non_add_bin_simps @ mult_minus_simps))
    1.38        THEN ALLGOALS (simp_tac (num_ss' addsimps minus_from_mult_simps @ add_ac @ mult_ac))
    1.39      end
    1.40    fun numeral_simp_tac ss =
    1.41 -    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
    1.42 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
    1.43    val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
    1.44    end;
    1.45