# HG changeset patch
# User haftmann
# Date 1242654336 -7200
# Node ID f8d4ac84334f763d7d9323b1ce52b5144e60b16a
# Parent  a324d214009cdc69ef64f6d68bb1d074abe148a2
generalized lemma map_of_zip_map

diff -r a324d214009c -r f8d4ac84334f src/HOL/Library/Enum.thy
--- a/src/HOL/Library/Enum.thy	Mon May 18 15:45:34 2009 +0200
+++ b/src/HOL/Library/Enum.thy	Mon May 18 15:45:36 2009 +0200
@@ -116,9 +116,8 @@
     by (simp add: length_n_lists)
 qed
 
-lemma map_of_zip_map:
-  fixes f :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>enum"
-  shows "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
+lemma map_of_zip_map: (*FIXME move to Map.thy*)
+  "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
   by (induct xs) (simp_all add: expand_fun_eq)
 
 lemma map_of_zip_enum_is_Some: