# 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 \| t \ 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