diff -r 11a0aa6cc677 -r 2ada2be850cb src/HOL/Library/RBT_Mapping.thy
--- a/src/HOL/Library/RBT_Mapping.thy	Thu Apr 12 13:47:21 2012 +0200
+++ b/src/HOL/Library/RBT_Mapping.thy	Fri Apr 13 11:45:30 2012 +0200
@@ -40,7 +40,7 @@
 
 lemma keys_Mapping [code]:
   "Mapping.keys (Mapping t) = set (keys t)"
-  by (simp add: RBT.keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys)
+  by (simp add: RBT.keys_def Mapping_def Mapping.keys_def lookup_def rbt_lookup_keys)
 
 lemma ordered_keys_Mapping [code]:
   "Mapping.ordered_keys (Mapping t) = keys t"
@@ -144,22 +144,22 @@
   @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"})
 
   \noindent
-  @{thm insert_is_rbt}\hfill(@{text "insert_is_rbt"})
+  @{thm rbt_insert_is_rbt}\hfill(@{text "rbt_insert_is_rbt"})
 
   \noindent
-  @{thm delete_is_rbt}\hfill(@{text "delete_is_rbt"})
+  @{thm rbt_delete_is_rbt}\hfill(@{text "delete_is_rbt"})
 
   \noindent
-  @{thm bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"})
+  @{thm rbt_bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"})
 
   \noindent
-  @{thm map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"})
+  @{thm rbt_map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"})
 
   \noindent
   @{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
 
   \noindent
-  @{thm union_is_rbt}\hfill(@{text "union_is_rbt"})
+  @{thm rbt_union_is_rbt}\hfill(@{text "union_is_rbt"})
 *}