--- a/src/HOL/ex/ROOT.ML Wed Jun 21 10:34:33 2000 +0200 +++ b/src/HOL/ex/ROOT.ML Wed Jun 21 15:58:23 2000 +0200 @@ -26,7 +26,7 @@ time_use_thy "IntRing"; -time_use "set.ML"; +time_use_thy "set"; time_use_thy "MT"; time_use_thy "Tarski";