diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Hyperreal/NatStar.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -186,7 +186,7 @@
 subsection{*Nonstandard Characterization of Induction*}
 
 definition
-  hSuc :: "hypnat => hypnat"
+  hSuc :: "hypnat => hypnat" where
   "hSuc n = n + 1"
 
 lemma starP: "(( *p* P) (star_n X)) = ({n. P (X n)} \<in> FreeUltrafilterNat)"