src/HOL/Lambda/ROOT.ML

--- a/src/HOL/Lambda/ROOT.ML	Thu Sep 06 11:39:43 2007 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Thu Sep 06 11:41:04 2007 +0200
@@ -8,7 +8,7 @@
 proofs := 2;
 
 no_document use_thys ["Accessible_Part", "Pretty_Int"];
-use_thys ["Eta", "StrongNorm"];
+use_thys ["Eta", "StrongNorm", "Standardization"];
 if HOL_proofs < 2 then
   warning "HOL proof terms required for running theory WeakNorm"
 else use_thy "WeakNorm";