src/HOL/Lambda/ROOT.ML

--- a/src/HOL/Lambda/ROOT.ML	Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
@@ -7,9 +7,8 @@
 Syntax.ambiguity_level := 100;
 proofs := 2;
 
-use_thy "Eta";
 no_document use_thy "Accessible_Part";
-use_thy "StrongNorm";
+use_thys ["Eta", "StrongNorm"];
 if HOL_proofs < 2 then
   warning "HOL proof terms required for running theory WeakNorm"
 else use_thy "WeakNorm";