--- a/src/HOL/NSA/Star.thy Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/NSA/Star.thy Tue Sep 07 10:05:19 2010 +0200
@@ -87,7 +87,7 @@
sequence) as a special case of an internal set*}
lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A"
-apply (drule expand_fun_eq [THEN iffD2])
+apply (drule ext_iff [THEN iffD2])
apply (simp add: starset_n_def starset_def star_of_def)
done
@@ -102,7 +102,7 @@
(*----------------------------------------------------------------*)
lemma starfun_n_starfun: "\<forall>n. (F n = f) ==> *fn* F = *f* f"
-apply (drule expand_fun_eq [THEN iffD2])
+apply (drule ext_iff [THEN iffD2])
apply (simp add: starfun_n_def starfun_def star_of_def)
done