celver code lemma avoid type ambiguity problem with Haskell
authorhaftmann
Tue, 16 Sep 2008 16:13:11 +0200
changeset 28245 9767dd8e1e54
parent 28244 f433e544a855
child 28246 8fc6ea9a2d8c
celver code lemma avoid type ambiguity problem with Haskell
src/HOL/Library/Enum.thy
--- a/src/HOL/Library/Enum.thy	Tue Sep 16 16:13:09 2008 +0200
+++ b/src/HOL/Library/Enum.thy	Tue Sep 16 16:13:11 2008 +0200
@@ -177,9 +177,9 @@
 
 end
 
-lemma [code func]:
-  "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>('a\<Colon>{enum, eq}) list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>{enum, eq} list)) enum)"
-  unfolding enum_fun_def ..
+lemma enum_fun_code [code func]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
+  in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
+  by (simp add: enum_fun_def Let_def)
 
 instantiation unit :: enum
 begin