--- a/src/HOL/Library/RBT.thy Wed Jun 01 22:35:51 2016 +0200
+++ b/src/HOL/Library/RBT.thy Thu Jun 02 08:34:23 2016 +0200
@@ -233,8 +233,8 @@
lifting_forget rbt.lifting
hide_const (open) impl_of empty lookup keys entries bulkload delete map fold union insert map_entry foldi
- is_empty
+ is_empty filter
hide_fact (open) empty_def lookup_def keys_def entries_def bulkload_def delete_def map_def fold_def
- union_def insert_def map_entry_def foldi_def is_empty_def
+ union_def insert_def map_entry_def foldi_def is_empty_def filter_def
end