# HG changeset patch
# User nipkow
# Date 1529052312 -7200
# Node ID 41de07c7a0f360565ed015e2cae5e833a0c09480
# Parent  6d0f1a5a16ea84b522872457f9294db7efa61e45
Map.empty now qualified to avoid name clashes

diff -r 6d0f1a5a16ea -r 41de07c7a0f3 NEWS
--- a/NEWS	Thu Jun 14 17:50:23 2018 +0200
+++ b/NEWS	Fri Jun 15 10:45:12 2018 +0200
@@ -320,6 +320,8 @@
 
   - list comprehension syntax now supports tuple patterns in "pat <- xs"
 
+* Theory Map: "empty" must now be qualified as "Map.empty".
+
 * Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
 
 * Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
diff -r 6d0f1a5a16ea -r 41de07c7a0f3 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Thu Jun 14 17:50:23 2018 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Fri Jun 15 10:45:12 2018 +0200
@@ -166,7 +166,7 @@
 lemma rbt_lookup_rbt_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> rbt_lookup t k = None"
 by (induct t) auto
 
-lemma rbt_lookup_Empty: "rbt_lookup Empty = empty"
+lemma rbt_lookup_Empty: "rbt_lookup Empty = Map.empty"
 by (rule ext) simp
 
 end
diff -r 6d0f1a5a16ea -r 41de07c7a0f3 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Thu Jun 14 17:50:23 2018 +0200
+++ b/src/HOL/Map.thy	Fri Jun 15 10:45:12 2018 +0200
@@ -826,4 +826,6 @@
   qed
 qed
 
+hide_const (open) Map.empty
+
 end