# HG changeset patch
# User wenzelm
# Date 1275505948 -7200
# Node ID 1fad5b94c0ae230f1c6395fa7627006ede9995d3
# Parent  5c0499f4f4c86aaefb3f38f92efc763215e53dcf
replaced ML pokes by explicit usedir -p;
prefer -q 0 for proof terms, which avoids overhead of proof promises, while exploiting implicit parallelism of internal normalization;

diff -r 5c0499f4f4c8 -r 1fad5b94c0ae src/HOL/Extraction/ROOT.ML
--- a/src/HOL/Extraction/ROOT.ML	Wed Jun 02 18:48:30 2010 +0200
+++ b/src/HOL/Extraction/ROOT.ML	Wed Jun 02 21:12:28 2010 +0200
@@ -1,6 +1,4 @@
 (* Examples for program extraction in Higher-Order Logic *)
 
-Proofterm.proofs := 2;
-
 no_document use_thys ["Efficient_Nat", "~~/src/HOL/Number_Theory/UniqueFactorization"];
 use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];
diff -r 5c0499f4f4c8 -r 1fad5b94c0ae src/HOL/Import/ROOT.ML
--- a/src/HOL/Import/ROOT.ML	Wed Jun 02 18:48:30 2010 +0200
+++ b/src/HOL/Import/ROOT.ML	Wed Jun 02 21:12:28 2010 +0200
@@ -1,8 +1,5 @@
 (*  Title:      HOL/Import/ROOT.ML
-    ID:         $Id$
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
-Proofterm.proofs := 0;
-use_thy "HOL4Compat";
-use_thy "HOL4Syntax";
+use_thys ["HOL4Compat", "HOL4Syntax"];
diff -r 5c0499f4f4c8 -r 1fad5b94c0ae src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jun 02 18:48:30 2010 +0200
+++ b/src/HOL/IsaMakefile	Wed Jun 02 21:12:28 2010 +0200
@@ -506,7 +506,7 @@
 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
@@ -857,7 +857,7 @@
   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
@@ -942,7 +942,7 @@
   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
diff -r 5c0499f4f4c8 -r 1fad5b94c0ae src/HOL/Lambda/ROOT.ML
--- a/src/HOL/Lambda/ROOT.ML	Wed Jun 02 18:48:30 2010 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Wed Jun 02 21:12:28 2010 +0200
@@ -1,5 +1,4 @@
 Syntax.ambiguity_level := 100;
-Proofterm.proofs := 2;
 
 no_document use_thys ["Code_Integer"];
 use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"];