# HG changeset patch
# User berghofe
# Date 1057331366 -7200
# Node ID f24b2818c1e7b442df9508a660863cd3bb248f7e
# Parent  7b34f58b1b81894b14816f8e2227beb415caa84d
Added check for HOL_proofs: Theory WeakNorm is skipped if HOL image has been
compiled without proof objects.

diff -r 7b34f58b1b81 -r f24b2818c1e7 src/HOL/Lambda/ROOT.ML
--- a/src/HOL/Lambda/ROOT.ML	Thu Jul 03 18:07:50 2003 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Fri Jul 04 17:09:26 2003 +0200
@@ -12,4 +12,6 @@
 time_use_thy "Eta";
 no_document time_use_thy "Accessible_Part";
 time_use_thy "StrongNorm";
-time_use_thy "WeakNorm";
+if HOL_proofs < 2 then
+  warning "HOL proof terms required for running theory WeakNorm"
+else time_use_thy "WeakNorm";