author | haftmann |
Thu, 18 Nov 2010 18:53:36 +0100 | |
changeset 40612 | 7ae5b89d8913 |
parent 40611 | 9eb0a9dd186e |
child 40613 | 23626b388e07 |
--- 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)"