src/HOL/Hyperreal/Transcendental.thy

--- a/src/HOL/Hyperreal/Transcendental.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -2473,7 +2473,7 @@
 by (erule DERIV_fun_exp)
 
 lemma STAR_exp_ln: "0 < z ==> ( *f* (%x. exp (ln x))) z = z"
-apply (rule_tac z = z in eq_Abs_hypreal)
+apply (rule_tac z = z in eq_Abs_star)
 apply (auto simp add: starfun hypreal_zero_def hypreal_less)
 done