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";