--- 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