src/ZF/arith_data.ML
changeset 17877 67d5ab1cb0d8
parent 16973 b2a894562b8f
child 17956 369e2af8ee45
     1.1 --- a/src/ZF/arith_data.ML	Mon Oct 17 23:10:13 2005 +0200
     1.2 +++ b/src/ZF/arith_data.ML	Mon Oct 17 23:10:15 2005 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4  (*Final simplification: cancel + and **)
     1.5  fun simplify_meta_eq rules ss =
     1.6      mk_meta_eq o
     1.7 -    simplify (Simplifier.inherit_bounds ss FOL_ss addeqcongs[eq_cong2,iff_cong2]
     1.8 +    simplify (Simplifier.inherit_context ss FOL_ss addeqcongs[eq_cong2,iff_cong2]
     1.9                       delsimps iff_simps (*these could erase the whole rule!*)
    1.10                       addsimps rules);
    1.11  
    1.12 @@ -146,11 +146,11 @@
    1.13    val norm_tac_ss1      = ZF_ss addsimps add_0s @ add_succs @ mult_1s @ add_ac
    1.14    val norm_tac_ss2      = ZF_ss addsimps add_0s @ mult_1s @ add_ac @ mult_ac @ tc_rules @ natifys
    1.15    fun norm_tac ss =
    1.16 -    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
    1.17 -    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
    1.18 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
    1.19 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
    1.20    val numeral_simp_tac_ss = ZF_ss addsimps add_0s @ tc_rules @ natifys
    1.21    fun numeral_simp_tac ss =
    1.22 -    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss numeral_simp_tac_ss))
    1.23 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss numeral_simp_tac_ss))
    1.24    val simplify_meta_eq  = simplify_meta_eq final_rules
    1.25    end;
    1.26