# HG changeset patch
# User haftmann
# Date 1291811690 -3600
# Node ID 286255f131bf725fce4739bb66e8c144c291c208
# Parent  07b454783ed8074884ba1e9164d1f84ec1dd0536
hide popular names R and B

diff -r 07b454783ed8 -r 286255f131bf src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Wed Dec 08 08:33:04 2010 +0100
+++ b/src/HOL/Library/RBT_Impl.thy	Wed Dec 08 13:34:50 2010 +0100
@@ -1079,6 +1079,6 @@
   then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev)
 qed
 
-hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
+hide_const (open) R B Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
 
 end