src/FOL/simpdata.ML
changeset 17875 d81094515061
parent 17325 d9d50222808e
child 17892 62c397c17d18
     1.1 --- a/src/FOL/simpdata.ML	Mon Oct 17 19:19:29 2005 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Mon Oct 17 23:10:10 2005 +0200
     1.3 @@ -339,7 +339,7 @@
     1.4  
     1.5  fun unfold_tac ss ths =
     1.6    ALLGOALS (full_simp_tac
     1.7 -    (Simplifier.inherit_bounds ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
     1.8 +    (Simplifier.inherit_context ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
     1.9  
    1.10  
    1.11  (*intuitionistic simprules only*)
    1.12 @@ -360,7 +360,7 @@
    1.13  (*classical simprules too*)
    1.14  val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
    1.15  
    1.16 -val simpsetup = [fn thy => (simpset_ref_of thy := FOL_ss; thy)];
    1.17 +val simpsetup = [fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy)];
    1.18  
    1.19  
    1.20  (*** integration of simplifier with classical reasoner ***)