--- a/src/HOL/NSA/NSComplex.thy Tue Mar 26 12:20:57 2013 +0100
+++ b/src/HOL/NSA/NSComplex.thy Tue Mar 26 12:20:58 2013 +0100
@@ -6,7 +6,7 @@
header{*Nonstandard Complex Numbers*}
theory NSComplex
-imports Complex NSA
+imports NSA
begin
type_synonym hcomplex = "complex star"