1.1 --- a/src/HOL/Extraction/ROOT.ML	Wed Jun 02 18:48:30 2010 +0200
     1.2 +++ b/src/HOL/Extraction/ROOT.ML	Wed Jun 02 21:12:28 2010 +0200
     1.3 @@ -1,6 +1,4 @@
     1.4  (* Examples for program extraction in Higher-Order Logic *)
     1.5  
     1.6 -Proofterm.proofs := 2;
     1.7 -
     1.8  no_document use_thys ["Efficient_Nat", "~~/src/HOL/Number_Theory/UniqueFactorization"];
     1.9  use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];

     2.1 --- a/src/HOL/Import/ROOT.ML	Wed Jun 02 18:48:30 2010 +0200
     2.2 +++ b/src/HOL/Import/ROOT.ML	Wed Jun 02 21:12:28 2010 +0200
     2.3 @@ -1,8 +1,5 @@
     2.4  (*  Title:      HOL/Import/ROOT.ML
     2.5 -    ID:         $Id$
     2.6      Author:     Sebastian Skalberg (TU Muenchen)
     2.7  *)
     2.8  
     2.9 -Proofterm.proofs := 0;
    2.10 -use_thy "HOL4Compat";
    2.11 -use_thy "HOL4Syntax";
    2.12 +use_thys ["HOL4Compat", "HOL4Syntax"];

     3.1 --- a/src/HOL/IsaMakefile	Wed Jun 02 18:48:30 2010 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Wed Jun 02 21:12:28 2010 +0200
     3.3 @@ -506,7 +506,7 @@
     3.4  HOL-Import: HOL $(LOG)/HOL-Import.gz
     3.5  
     3.6  $(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES)
     3.7 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Import
     3.8 +	@$(ISABELLE_TOOL) usedir -p 0 $(OUT)/HOL Import
     3.9  
    3.10  
    3.11  ## HOL-Generate-HOL
    3.12 @@ -857,7 +857,7 @@
    3.13    Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy	\
    3.14    Lambda/StrongNorm.thy Lambda/Type.thy Lambda/WeakNorm.thy		\
    3.15    Lambda/ROOT.ML Lambda/document/root.bib Lambda/document/root.tex
    3.16 -	@$(ISABELLE_TOOL) usedir -g true -m no_brackets $(OUT)/HOL-Proofs Lambda
    3.17 +	@$(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda
    3.18  
    3.19  
    3.20  ## HOL-Prolog
    3.21 @@ -942,7 +942,7 @@
    3.22    Extraction/Pigeonhole.thy Extraction/QuotRem.thy Extraction/ROOT.ML	\
    3.23    Extraction/Util.thy Extraction/Warshall.thy				\
    3.24    Extraction/document/root.tex Extraction/document/root.bib
    3.25 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL-Proofs Extraction
    3.26 +	@$(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction
    3.27  
    3.28  
    3.29  ## HOL-IOA

     4.1 --- a/src/HOL/Lambda/ROOT.ML	Wed Jun 02 18:48:30 2010 +0200
     4.2 +++ b/src/HOL/Lambda/ROOT.ML	Wed Jun 02 21:12:28 2010 +0200
     4.3 @@ -1,5 +1,4 @@
     4.4  Syntax.ambiguity_level := 100;
     4.5 -Proofterm.proofs := 2;
     4.6  
     4.7  no_document use_thys ["Code_Integer"];
     4.8  use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"];