src/HOL/Library/RBT_Mapping.thy

--- a/src/HOL/Library/RBT_Mapping.thy	Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Library/RBT_Mapping.thy	Fri Jun 22 20:31:49 2018 +0200
@@ -113,7 +113,7 @@
 text \<open>
   This theory defines abstract red-black trees as an efficient
   representation of finite maps, backed by the implementation
-  in @{theory RBT_Impl}.
+  in @{theory "HOL-Library.RBT_Impl"}.
 \<close>
 
 subsection \<open>Data type and invariant\<close>