--- 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"