src/HOL/Library/RBT_Impl.thy

--- a/src/HOL/Library/RBT_Impl.thy	Thu Jun 14 17:50:23 2018 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Fri Jun 15 10:45:12 2018 +0200
@@ -166,7 +166,7 @@
 lemma rbt_lookup_rbt_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> rbt_lookup t k = None"
 by (induct t) auto
 
-lemma rbt_lookup_Empty: "rbt_lookup Empty = empty"
+lemma rbt_lookup_Empty: "rbt_lookup Empty = Map.empty"
 by (rule ext) simp
 
 end