--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy Fri Jun 15 13:02:12 2018 +0200
@@ -90,7 +90,7 @@
done
lemma map_of_map_as_map_upd:
- "distinct (map f zs) \<Longrightarrow> map_of (map (\<lambda> p. (f p, g p)) zs) = empty (map f zs [\<mapsto>] map g zs)"
+ "distinct (map f zs) \<Longrightarrow> map_of (map (\<lambda> p. (f p, g p)) zs) = Map.empty (map f zs [\<mapsto>] map g zs)"
by (induct zs) auto
(* In analogy to Map.map_of_SomeD *)