src/HOL/Extraction/ROOT.ML

--- a/src/HOL/Extraction/ROOT.ML	Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/Extraction/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
@@ -8,8 +8,5 @@
   warning "HOL proof terms required for running extraction examples"
 else
   (proofs := 2;
-   time_use_thy "QuotRem";
-   time_use_thy "Warshall";
-   time_use_thy "Higman";
    no_document time_use_thy "Efficient_Nat";
-   time_use_thy "Pigeonhole");
+   use_thys ["QuotRem", "Warshall", "Higman", "Pigeonhole"]);