src/HOL/NSA/NSComplex.thy

--- a/src/HOL/NSA/NSComplex.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/NSA/NSComplex.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -9,7 +9,7 @@
 imports Complex NSA
 begin
 
-types hcomplex = "complex star"
+type_synonym hcomplex = "complex star"
 
 abbreviation
   hcomplex_of_complex :: "complex => complex star" where