--- 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)));