diff -r 41de07c7a0f3 -r c34aa23a1fb6 src/HOL/MicroJava/J/Exceptions.thy
--- a/src/HOL/MicroJava/J/Exceptions.thy	Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/MicroJava/J/Exceptions.thy	Fri Jun 15 13:02:12 2018 +0200
@@ -10,7 +10,7 @@
   "blank G C \<equiv> (C,init_vars (fields(G,C)))" 
 
 definition start_heap :: "'c prog \<Rightarrow> aheap" where
-  "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))
+  "start_heap G \<equiv> Map.empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))
                         (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))
                         (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"