diff -r 41de07c7a0f3 -r c34aa23a1fb6 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Jun 15 13:02:12 2018 +0200
@@ -83,7 +83,7 @@
                     list.map map_of.simps map_upds_Cons list.sel)
   done
 
-lemma map_of_as_map_upds: "map_of (rev xs) = empty ((map fst xs) [\<mapsto>] (map snd xs))"
+lemma map_of_as_map_upds: "map_of (rev xs) = Map.empty ((map fst xs) [\<mapsto>] (map snd xs))"
   by (rule map_of_append [of _ "[]", simplified])
 
 lemma map_of_rev: "unique xs \<Longrightarrow> map_of (rev xs) = map_of xs"
@@ -105,7 +105,7 @@
   done
 
 lemma map_upds_takeWhile [rule_format]:
-  "\<forall>ks. (empty(rev ks[\<mapsto>]rev xs)) k = Some x \<longrightarrow> length ks = length xs \<longrightarrow>
+  "\<forall>ks. (Map.empty(rev ks[\<mapsto>]rev xs)) k = Some x \<longrightarrow> length ks = length xs \<longrightarrow>
     xs ! length (takeWhile (\<lambda>z. z \<noteq> k) ks) = x"
   apply (induct xs)
    apply simp
@@ -114,7 +114,7 @@
    apply (clarify)
    apply (drule_tac x=kr in spec)
    apply (simp only: rev.simps)
-   apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
+   apply (subgoal_tac "(Map.empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = Map.empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
     apply (simp split:if_split_asm)
    apply (simp add: map_upds_append [symmetric])
   apply (case_tac ks)