--- a/src/HOL/Induct/ROOT.ML Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/Induct/ROOT.ML Tue Jul 31 22:21:20 2007 +0200
@@ -1,16 +1,6 @@
(* $Id$ *)
-time_use_thy "Mutil";
-time_use_thy "QuoDataType";
-time_use_thy "QuoNestedDataType";
-time_use_thy "Term";
-time_use_thy "ABexp";
-time_use_thy "Tree";
-time_use_thy "Ordinals";
-time_use_thy "Sigma_Algebra";
-time_use_thy "Comb";
-time_use_thy "PropLog";
-time_use_thy "SList";
-time_use_thy "LFilter";
-time_use_thy "Com";
+use_thys ["Mutil", "QuoDataType", "QuoNestedDataType", "Term",
+ "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog",
+ "SList", "LFilter", "Com"];