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