# HG changeset patch
# User Andreas Lochbihler <mail@andreas-lochbihler.de>
# Date 1612079387 -3600
# Node ID 87e3c180044a4289917c175348767abb0f346587
# Parent  bfa9f646f5ae358d62b92b432e7504c9f273cce9
hide the internal abbreviations MR and MB

diff -r bfa9f646f5ae -r 87e3c180044a src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Fri Jan 29 13:06:29 2021 +0100
+++ b/src/HOL/Library/RBT_Impl.thy	Sun Jan 31 08:49:47 2021 +0100
@@ -1883,8 +1883,8 @@
 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)"
@@ -3082,6 +3082,6 @@
      (\<^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