src/HOL/Tools/record_package.ML
changeset 17875 d81094515061
parent 17616 f526e2b9fe9e
child 17892 62c397c17d18
     1.1 --- a/src/HOL/Tools/record_package.ML	Mon Oct 17 19:19:29 2005 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Mon Oct 17 23:10:10 2005 +0200
     1.3 @@ -826,7 +826,7 @@
     1.4                   | NONE => extsplits)
     1.5    in
     1.6      quick_and_dirty_prove true sg [] prop
     1.7 -      (fn _ => simp_tac (Simplifier.inherit_bounds ss simpset addsimps thms) 1)
     1.8 +      (fn _ => simp_tac (Simplifier.inherit_context ss simpset addsimps thms) 1)
     1.9    end;
    1.10  
    1.11  
    1.12 @@ -1069,7 +1069,7 @@
    1.13         let
    1.14           fun prove prop =
    1.15             quick_and_dirty_prove true sg [] prop
    1.16 -             (fn _ => simp_tac (Simplifier.inherit_bounds ss (get_simpset sg)
    1.17 +             (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset sg)
    1.18                 addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1);
    1.19  
    1.20           fun mkeq (lr,Teq,(sel,Tsel),x) i =
    1.21 @@ -2106,8 +2106,8 @@
    1.22   [RecordsData.init,
    1.23    Theory.add_trfuns ([], parse_translation, [], []),
    1.24    Theory.add_advanced_trfuns ([], adv_parse_translation, [], []),
    1.25 -  Simplifier.change_simpset_of Simplifier.addsimprocs
    1.26 -    [record_simproc, record_upd_simproc, record_eq_simproc]];
    1.27 +  (fn thy => (Simplifier.change_simpset_of thy
    1.28 +    (fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); thy))];
    1.29  
    1.30  (* outer syntax *)
    1.31