--- a/src/HOL/Hoare/Separation.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Hoare/Separation.thy Fri Jun 15 13:02:12 2018 +0200
@@ -20,7 +20,7 @@
where "h1 \<bottom> h2 \<longleftrightarrow> dom h1 \<inter> dom h2 = {}"
definition is_empty :: "heap \<Rightarrow> bool"
- where "is_empty h \<longleftrightarrow> h = empty"
+ where "is_empty h \<longleftrightarrow> h = Map.empty"
definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
where "singl h x y \<longleftrightarrow> dom h = {x} & h x = Some y"