diff -r ab93d0190a5d -r 1165fe965da8 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Jul 19 14:38:29 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Tue Jul 19 14:38:48 2011 +0200
@@ -55,7 +55,7 @@
   instance ..
 end
 
-definition "ereal_of_enat n = (case n of Fin n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
+definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
 
 declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
 declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]