diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Orderings.thy	Wed Aug 25 18:36:22 2010 +0200
@@ -566,7 +566,7 @@
 fun add_simprocs procs thy =
   Simplifier.map_simpset (fn ss => ss
     addsimprocs (map (fn (name, raw_ts, proc) =>
-      Simplifier.simproc thy name raw_ts proc) procs)) thy;
+      Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
 fun add_solver name tac =
   Simplifier.map_simpset (fn ss => ss addSolver
     mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));