src/HOL/Map.thy

 lemma map_of_append[simp]: "map_of (xs @ ys) = map_of ys ++ map_of xs"
 unfolding map_add_def
 apply (induct xs)
  apply simp
 apply (rule ext)
-apply (simp split add: option.split)
+apply (simp split: option.split)
 done
 
 lemma finite_range_map_of_map_add:
   "finite (range f) \<Longrightarrow> finite (range (f ++ map_of l))"
 apply (induct l)