src/HOL/Extraction/ROOT.ML

 
 if HOL_proofs < 2 then
   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"]);