diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -10,7 +10,7 @@
 imports HyperNat Real
 begin
 
-types hypreal = "real star"
+type_synonym hypreal = "real star"
 
 abbreviation
   hypreal_of_real :: "real => real star" where