Map.empty no longer output abbreviation; %_. None is shorter and requires no explanation

--- a/NEWS	Thu Feb 23 15:37:17 2023 +0100
+++ b/NEWS	Thu Feb 23 22:04:32 2023 +0100
@@ -51,6 +51,9 @@
   - Renamed lemma inj_on_strict_subset to image_strict_mono.
     Minor INCOMPATIBILITY.
 
+* Theory HOL.Map:
+  - Map.empty has been demoted to an input abbreviation only
+
 * Theory "HOL.Relation":
   - Added predicates irrefl_on and irreflp_on and redefined irrefl and
     irreflp to be abbreviations. Lemmas irrefl_def and irreflp_def are

--- a/src/HOL/Map.thy	Thu Feb 23 15:37:17 2023 +0100
+++ b/src/HOL/Map.thy	Thu Feb 23 22:04:32 2023 +0100
@@ -14,7 +14,7 @@
 
 type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr "\<rightharpoonup>" 0)
 
-abbreviation
+abbreviation (input)
   empty :: "'a \<rightharpoonup> 'b" where
   "empty \<equiv> \<lambda>x. None"