diff -r ba543692bfa1 -r 2c31dd358c21 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Sat Sep 16 02:40:00 2006 +0200
@@ -362,7 +362,6 @@
 lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
 apply (cases x)
 apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n], auto)
 apply (rule_tac x = "exp u" in exI)
 apply ultra
 done