--- 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
--- 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
--- 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