src/HOL/Complex/ROOT.ML

--- a/src/HOL/Complex/ROOT.ML	Mon Dec 29 06:49:26 2003 +0100
+++ b/src/HOL/Complex/ROOT.ML	Thu Jan 01 10:06:32 2004 +0100
@@ -5,6 +5,6 @@
 The Complex Numbers
 *)
 
-with_path "../Real" use_thy "Real";
+with_path "../Real"      use_thy "Real";
 with_path "../Hyperreal" use_thy "Hyperreal";
 time_use_thy "Complex_Main";