1.1 --- a/src/HOL/Library/Enum.thy	Mon May 18 15:45:34 2009 +0200
     1.2 +++ b/src/HOL/Library/Enum.thy	Mon May 18 15:45:36 2009 +0200
     1.3 @@ -116,9 +116,8 @@
     1.4      by (simp add: length_n_lists)
     1.5  qed
     1.6  
     1.7 -lemma map_of_zip_map:
     1.8 -  fixes f :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>enum"
     1.9 -  shows "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
    1.10 +lemma map_of_zip_map: (*FIXME move to Map.thy*)
    1.11 +  "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
    1.12    by (induct xs) (simp_all add: expand_fun_eq)
    1.13  
    1.14  lemma map_of_zip_enum_is_Some: