# HG changeset patch
# User haftmann
# Date 1290102816 -3600
# Node ID 7ae5b89d89134307c9c1876c88f11e4a16a0b385
# Parent  9eb0a9dd186e1da534e388d9c86a656cd3f65d70
proper qualification needed due to shadowing on theory merge

diff -r 9eb0a9dd186e -r 7ae5b89d8913 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Thu Nov 18 17:06:02 2010 +0100
+++ b/src/HOL/Library/RBT.thy	Thu Nov 18 18:53:36 2010 +0100
@@ -144,7 +144,7 @@
 
 lemma lookup_map [simp]:
   "lookup (map f t) k = Option.map (f k) (lookup t k)"
-  by (simp add: map_def lookup_RBT lookup_map lookup_impl_of)
+  by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
 
 lemma fold_fold:
   "fold f t = More_List.fold (prod_case f) (entries t)"