diff -r c6f35921056e -r ab93d0190a5d src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:37:49 2011 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:38:29 2011 +0200
@@ -47,7 +47,6 @@
   qed
 qed (auto simp add: Fin_def infinity_enat_def Abs_enat_inject)
 
-declare [[coercion_enabled]]
 declare [[coercion "Fin::nat\<Rightarrow>enat"]]
 
 lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = Fin i)"