diff -r 93c6f0da5c70 -r aee949f6642d src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Sun Oct 16 09:31:05 2016 +0200
@@ -1416,7 +1416,7 @@
         moreover note feven[unfolded feven_def]
           (* FIXME: why does by(rule feven[unfolded feven_def]) not work? *)
         ultimately have "P (2 * (n div 2)) kvs" by -
-        thus ?thesis using True by (metis div_mod_equality' minus_nat.diff_0 mult.commute)
+        thus ?thesis using True by (metis minus_mod_eq_div_mult [symmetric] minus_nat.diff_0 mult.commute)
       next
         case False note ge0
         moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp
@@ -1462,7 +1462,7 @@
         moreover note geven[unfolded geven_def]
         ultimately have "Q (2 * (n div 2)) kvs" by -
         thus ?thesis using True 
-          by(metis div_mod_equality' minus_nat.diff_0 mult.commute)
+          by(metis minus_mod_eq_div_mult [symmetric] minus_nat.diff_0 mult.commute)
       next
         case False note ge0
         moreover from "2.prems" have n2: "n div 2 \<le> length kvs" by simp