src/HOL/Library/RBT_Impl.thy

   "small_rbt t \<longleftrightarrow> bheight t < 4"
 
 definition flip_rbt :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" where
   "flip_rbt t1 t2 \<longleftrightarrow> bheight t2 < bheight t1"
 
-abbreviation MR where "MR l a b r \<equiv> Branch RBT_Impl.R l a b r"
-abbreviation MB where "MB l a b r \<equiv> Branch RBT_Impl.B l a b r"
+abbreviation (input) MR where "MR l a b r \<equiv> Branch RBT_Impl.R l a b r"
+abbreviation (input) MB where "MB l a b r \<equiv> Branch RBT_Impl.B l a b r"
 
 fun rbt_baliL :: "('a, 'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
   "rbt_baliL (MR (MR t1 a b t2) a' b' t3) a'' b'' t4 = MR (MB t1 a b t2) a' b' (MB t3 a'' b'' t4)"
 | "rbt_baliL (MR t1 a b (MR t2 a' b' t3)) a'' b'' t4 = MR (MB t1 a b t2) a' b' (MB t3 a'' b'' t4)"
 | "rbt_baliL t1 a b t2 = MB t1 a b t2"

      (\<^const_name>\<open>rbt_union\<close>, SOME \<^typ>\<open>('a::linorder,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt\<close>),
      (\<^const_name>\<open>rbt_map_entry\<close>, SOME \<^typ>\<open>'a::linorder \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt\<close>),
      (\<^const_name>\<open>rbt_bulkload\<close>, SOME \<^typ>\<open>('a \<times> 'b) list \<Rightarrow> ('a::linorder,'b) rbt\<close>)]
 \<close>
 
-hide_const (open) R B Empty entries keys fold gen_keys gen_entries
+hide_const (open) MR MB R B Empty entries keys fold gen_keys gen_entries
 
 end