1.1 --- a/src/HOL/Library/RBT.thy	Thu Nov 18 17:06:02 2010 +0100
     1.2 +++ b/src/HOL/Library/RBT.thy	Thu Nov 18 18:53:36 2010 +0100
     1.3 @@ -144,7 +144,7 @@
     1.4  
     1.5  lemma lookup_map [simp]:
     1.6    "lookup (map f t) k = Option.map (f k) (lookup t k)"
     1.7 -  by (simp add: map_def lookup_RBT lookup_map lookup_impl_of)
     1.8 +  by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
     1.9  
    1.10  lemma fold_fold:
    1.11    "fold f t = More_List.fold (prod_case f) (entries t)"