src/HOL/Library/RBT_Impl.thy

     "lookup (foldl (\<lambda>t (k, v). insert k v t) Empty (rev xs)) = lookup Empty ++ map_of xs"
      by (simp add: `ys = rev xs`)
   then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def)
 qed
 
-hide (open) const Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
+hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
 
 end