1.1 --- a/src/HOL/Orderings.thy	Wed Aug 25 18:19:04 2010 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Wed Aug 25 18:36:22 2010 +0200
     1.3 @@ -566,7 +566,7 @@
     1.4  fun add_simprocs procs thy =
     1.5    Simplifier.map_simpset (fn ss => ss
     1.6      addsimprocs (map (fn (name, raw_ts, proc) =>
     1.7 -      Simplifier.simproc thy name raw_ts proc) procs)) thy;
     1.8 +      Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
     1.9  fun add_solver name tac =
    1.10    Simplifier.map_simpset (fn ss => ss addSolver
    1.11      mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));