diff -r 56fa33537869 -r 0d31c0546286 src/HOL/Metis_Examples/Binary_Tree.thy
--- a/src/HOL/Metis_Examples/Binary_Tree.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy	Fri Feb 14 07:53:45 2014 +0100
@@ -130,14 +130,14 @@
 
 lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
 apply (induct t)
- apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1))
+ apply (metis bt_map.simps(1) list.map(1) preorder.simps(1))
 by simp
 
 lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
 proof (induct t)
   case Lf thus ?case
   proof -
-    have "map f [] = []" by (metis map.simps(1))
+    have "map f [] = []" by (metis list.map(1))
     hence "map f [] = inorder Lf" by (metis inorder.simps(1))
     hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1))
     thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1))