src/HOL/Orderings.thy
changeset 42795 66fcc9882784
parent 42287 d98eb048a2e4
child 43596 78211f66cf8d
     1.1 --- a/src/HOL/Orderings.thy	Fri May 13 23:24:06 2011 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri May 13 23:58:40 2011 +0200
     1.3 @@ -564,11 +564,12 @@
     1.4    handle THM _ => NONE;
     1.5  
     1.6  fun add_simprocs procs thy =
     1.7 -  Simplifier.map_simpset (fn ss => ss
     1.8 +  Simplifier.map_simpset_global (fn ss => ss
     1.9      addsimprocs (map (fn (name, raw_ts, proc) =>
    1.10        Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
    1.11 +
    1.12  fun add_solver name tac =
    1.13 -  Simplifier.map_simpset (fn ss => ss addSolver
    1.14 +  Simplifier.map_simpset_global (fn ss => ss addSolver
    1.15      mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));
    1.16  
    1.17  in