diff -r de51a86fc903 -r cc97b347b301 src/HOL/Metis_Examples/Binary_Tree.thy
--- a/src/HOL/Metis_Examples/Binary_Tree.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -66,7 +66,7 @@
   qed
 next
   case (Br a t1 t2) thus ?case
-    by (metis n_leaves.simps(2) nat_add_commute reflect.simps(2))
+    by (metis n_leaves.simps(2) add.commute reflect.simps(2))
 qed
 
 lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
@@ -74,7 +74,7 @@
   case Lf thus ?case by (metis reflect.simps(1))
 next
   case (Br a t1 t2) thus ?case
-    by (metis add_commute n_nodes.simps(2) reflect.simps(2))
+    by (metis add.commute n_nodes.simps(2) reflect.simps(2))
 qed
 
 lemma depth_reflect: "depth (reflect t) = depth t"