# HG changeset patch
# User kleing
# Date 1053703193 -7200
# Node ID 61093a0ac760ebcabb838bc4caf58cdbbf6e4dd9
# Parent  c2d981d222bf374ef18151c83c450ddac5325c02
make it possible to switch off proof objects for HOL image

diff -r c2d981d222bf -r 61093a0ac760 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri May 23 17:18:10 2003 +0200
+++ b/src/HOL/IsaMakefile	Fri May 23 17:19:53 2003 +0200
@@ -4,6 +4,9 @@
 # IsaMakefile for HOL
 #
 
+# for overriding proof objects in HOL image
+HOL_PROOF_OBJECTS="-p 2"
+
 ## targets
 
 default: HOL
@@ -109,7 +112,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 -p 2 $(OUT)/Pure HOL
+	@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
 
 
 ## HOL-Complex-HahnBanach