diff -r 6a6d8004322f -r c2f672be8522 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Sun Sep 17 16:44:05 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Sun Sep 17 16:44:51 2006 +0200
@@ -357,7 +357,8 @@
 lemma HFinite_hrabs_iff [iff]: "(abs (x::hypreal) \<in> HFinite) = (x \<in> HFinite)"
 by (simp add: HFinite_def)
 
-lemma HFinite_hnorm_iff [iff]: "(hnorm x \<in> HFinite) = (x \<in> HFinite)"
+lemma HFinite_hnorm_iff [iff]:
+  "(hnorm (x::hypreal) \<in> HFinite) = (x \<in> HFinite)"
 by (simp add: HFinite_def)
 
 lemma HFinite_number_of [simp]: "number_of w \<in> HFinite"