# HG changeset patch
# User kleing
# Date 1052918557 -7200
# Node ID fe031a7c75bcad55fe088e564d36d33dbd0fed6d
# Parent  ff6eb32b30a13279741230558409ec2c755fadd9
use proof objects for HOL by default

diff -r ff6eb32b30a1 -r fe031a7c75bc src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed May 14 14:20:55 2003 +0200
+++ b/src/HOL/IsaMakefile	Wed May 14 15:22:37 2003 +0200
@@ -109,8 +109,7 @@
   Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
   Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
   document/root.tex hologic.ML meson_lemmas.ML simpdata.ML thy_syntax.ML
-	@$(ISATOOL) usedir -b -g true $(OUT)/Pure HOL
-
+	@$(ISATOOL) usedir -b -g true -p 2 $(OUT)/Pure HOL
 
 
 ## HOL-Complex-HahnBanach