src/HOL/Orderings.thy
changeset 26496 49ae9456eba9
parent 26324 456f726a11e4
child 26796 c554b77061e5
     1.1 --- a/src/HOL/Orderings.thy	Sat Mar 29 19:24:57 2008 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Sat Mar 29 22:55:49 2008 +0100
     1.3 @@ -516,12 +516,12 @@
     1.4    handle THM _ => NONE;
     1.5  
     1.6  fun add_simprocs procs thy =
     1.7 -  (Simplifier.change_simpset_of thy (fn ss => ss
     1.8 +  Simplifier.map_simpset (fn ss => ss
     1.9      addsimprocs (map (fn (name, raw_ts, proc) =>
    1.10 -      Simplifier.simproc thy name raw_ts proc)) procs); thy);
    1.11 -fun add_solver name tac thy =
    1.12 -  (Simplifier.change_simpset_of thy (fn ss => ss addSolver
    1.13 -    (mk_solver' name (fn ss => tac (MetaSimplifier.prems_of_ss ss) (MetaSimplifier.the_context ss)))); thy);
    1.14 +      Simplifier.simproc thy name raw_ts proc) procs)) thy;
    1.15 +fun add_solver name tac =
    1.16 +  Simplifier.map_simpset (fn ss => ss addSolver
    1.17 +    mk_solver' name (fn ss => tac (Simplifier.prems_of_ss ss) (Simplifier.the_context ss)));
    1.18  
    1.19  in
    1.20    add_simprocs [