# HG changeset patch
# User blanchet
# Date 1425397065 -3600
# Node ID 55f5e1cbf2a756b651bf814e48be2a490dd7040f
# Parent  de392405a851743376358e0bca73f8f804612784
removed needless (and inconsistent) qualifier that messes up with Mirabelle

diff -r de392405a851 -r 55f5e1cbf2a7 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Library/RBT_Impl.thy	Tue Mar 03 16:37:45 2015 +0100
@@ -1195,7 +1195,7 @@
 done
 
 lemma rbtreeify_f_simps:
-  "rbtreeify_f 0 kvs = (RBT_Impl.Empty, kvs)"
+  "rbtreeify_f 0 kvs = (Empty, kvs)"
   "rbtreeify_f (Suc 0) ((k, v) # kvs) = 
   (Branch R Empty k v Empty, kvs)"
   "0 < n \<Longrightarrow> rbtreeify_f (2 * n) kvs =