src/HOL/Orderings.thy

      | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2}))
   end
   handle THM _ => NONE;
 
 fun add_simprocs procs thy =
-  (Simplifier.change_simpset_of thy (fn ss => ss
+  Simplifier.map_simpset (fn ss => ss
     addsimprocs (map (fn (name, raw_ts, proc) =>
-      Simplifier.simproc thy name raw_ts proc)) procs); thy);
-fun add_solver name tac thy =
-  (Simplifier.change_simpset_of thy (fn ss => ss addSolver
-    (mk_solver' name (fn ss => tac (MetaSimplifier.prems_of_ss ss) (MetaSimplifier.the_context ss)))); thy);
+      Simplifier.simproc 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.prems_of_ss ss) (Simplifier.the_context ss)));
 
 in
   add_simprocs [
        ("antisym le", ["(x::'a::order) <= y"], prove_antisym_le),
        ("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less)