src/HOL/NSA/NatStar.thy

--- a/src/HOL/NSA/NatStar.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/NSA/NatStar.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -115,7 +115,7 @@
   @{term real_of_nat} *}
 
 lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
-by transfer (simp add: ext_iff real_of_nat_def)
+by transfer (simp add: fun_eq_iff real_of_nat_def)
 
 lemma starfun_inverse_real_of_nat_eq:
      "N \<in> HNatInfinite