src/HOL/Complex/ROOT.ML

--- a/src/HOL/Complex/ROOT.ML	Sun Jul 22 23:23:39 2007 +0200
+++ b/src/HOL/Complex/ROOT.ML	Sun Jul 22 23:33:57 2007 +0200
@@ -5,9 +5,5 @@
 The Complex Numbers.
 *)
 
-no_document use_thy "Infinite_Set";
-no_document use_thy "Parity";
-
-with_path "../Real" use_thy "Float";
-with_path "../Hyperreal" use_thy "Hyperreal";
-use_thy "Complex_Main";
+no_document use_thys ["Infinite_Set", "Parity"];
+use_thys ["../Real/Float", "Complex_Main"];