src/HOL/Hyperreal/HSeries.thy

--- a/src/HOL/Hyperreal/HSeries.thy	Fri Dec 15 17:51:07 2006 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy	Sat Dec 16 19:37:07 2006 +0100
@@ -107,7 +107,7 @@
 (* FIXME: need lemma: hypreal_of_hypnat whn = omega - 1 *)
 (* maybe define omega = hypreal_of_hypnat whn + 1 *)
 apply (unfold star_class_defs omega_def hypnat_omega_def
-              hypreal_of_hypnat_def star_of_def)
+              of_hypnat_def star_of_def)
 apply (simp add: starfun_star_n starfun2_star_n real_of_nat_def)
 done