src/HOL/Orderings.thy

     addsimprocs (map (fn (name, raw_ts, proc) =>
       Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
 
 fun add_solver name tac =
   Simplifier.map_simpset_global (fn ss => ss addSolver
-    mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));
+    mk_solver name (fn ss => tac (Simplifier.the_context ss) (prems_of_ss ss)));
 
 in
   add_simprocs [
        ("antisym le", ["(x::'a::order) <= y"], prove_antisym_le),
        ("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less)