diff -r 6f79698f294d -r ba2bcae7aafd src/HOL/MetisExamples/BT.thy
--- a/src/HOL/MetisExamples/BT.thy	Thu Nov 22 14:51:34 2007 +0100
+++ b/src/HOL/MetisExamples/BT.thy	Fri Nov 23 17:37:56 2007 +0100
@@ -171,7 +171,7 @@
 lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
   apply (induct t)
   apply (metis One_nat_def Suc_eq_add_numeral_1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1))
-  apply (metis add_commute bt_map.simps(2) n_leaves.simps(2))
+  apply (metis bt_map.simps(2) n_leaves.simps(2))
   done
 
 
@@ -179,7 +179,7 @@
 lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
   apply (induct t)
   apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev_is_Nil_conv)
-  apply (metis append_eq_append_conv2 inorder.simps(1) postorder.simps(2) preorder.simps(2) reflect.simps(2) rev_append rev_is_rev_conv rev_singleton_conv rev_swap rotate_simps)
+  apply (metis Cons_eq_append_conv monoid_append.add_0_left postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rev_rev_ident)
   done
 
 ML {*ResAtp.problem_name := "BT__inorder_reflect"*}
@@ -193,7 +193,7 @@
 lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
   apply (induct t)
   apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev.simps(1))
-  apply (metis Cons_eq_appendI postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rotate1_def self_append_conv2)
+  apply (metis Cons_eq_appendI postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append self_append_conv2)
   done
 
 text {*