# HG changeset patch
# User haftmann
# Date 1221574391 -7200
# Node ID 9767dd8e1e540c86157f60433d638b2fad5e45db
# Parent  f433e544a855503a84f4356ee4a9095f3106e58a
celver code lemma avoid type ambiguity problem with Haskell

diff -r f433e544a855 -r 9767dd8e1e54 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