diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Hyperreal/HyperArith.thy
--- a/src/HOL/Hyperreal/HyperArith.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Hyperreal/HyperArith.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -34,7 +34,7 @@
 subsection{*Embedding the Naturals into the Hyperreals*}
 
 abbreviation
-  hypreal_of_nat   :: "nat => hypreal"
+  hypreal_of_nat :: "nat => hypreal" where
   "hypreal_of_nat == of_nat"
 
 lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"