--- a/src/ZF/ROOT.ML Mon Feb 11 21:32:10 2008 +0100 +++ b/src/ZF/ROOT.ML Mon Feb 11 21:32:11 2008 +0100 @@ -8,6 +8,5 @@ Paulson. *) -use_thy "Main"; -use_thy "Main_ZFC"; +use_thys ["Main", "Main_ZFC"];