diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Feb 12 08:37:06 2014 +0100
@@ -80,7 +80,7 @@
 apply (rule allI)
 apply (drule_tac x="a # ys" in spec)
 apply (simp only: rev.simps append_assoc append_Cons append_Nil
-  map.simps map_of.simps map_upds_Cons hd.simps tl.simps)
+  map.simps 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))"