src/HOL/Orderings.thy
changeset 38715 6513ea67d95d
parent 38705 aaee86c0e237
child 38786 e46e7a9cb622
     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)));