src/HOL/IsaMakefile

   Import/hol4rews.ML Import/import.ML Import/ROOT.ML
 
 HOL-Import: HOL $(LOG)/HOL-Import.gz
 
 $(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES)
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Import
+	@$(ISABELLE_TOOL) usedir -p 0 $(OUT)/HOL Import
 
 
 ## HOL-Generate-HOL
 
 HOL-Generate-HOL: HOL $(LOG)/HOL-Generate-HOL.gz

   Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy		\
   Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy	\
   Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy	\
   Lambda/StrongNorm.thy Lambda/Type.thy Lambda/WeakNorm.thy		\
   Lambda/ROOT.ML Lambda/document/root.bib Lambda/document/root.tex
-	@$(ISABELLE_TOOL) usedir -g true -m no_brackets $(OUT)/HOL-Proofs Lambda
+	@$(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda
 
 
 ## HOL-Prolog
 
 HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz

   Library/Efficient_Nat.thy Extraction/Euclid.thy			\
   Extraction/Greatest_Common_Divisor.thy Extraction/Higman.thy		\
   Extraction/Pigeonhole.thy Extraction/QuotRem.thy Extraction/ROOT.ML	\
   Extraction/Util.thy Extraction/Warshall.thy				\
   Extraction/document/root.tex Extraction/document/root.bib
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOL-Proofs Extraction
+	@$(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction
 
 
 ## HOL-IOA
 
 HOL-IOA: HOL $(LOG)/HOL-IOA.gz