1.1 --- a/src/HOL/Lambda/ROOT.ML	Mon Aug 06 11:45:39 2007 +0200
     1.2 +++ b/src/HOL/Lambda/ROOT.ML	Mon Aug 06 16:05:25 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  Syntax.ambiguity_level := 100;
     1.5  proofs := 2;
     1.6  
     1.7 -no_document use_thy "Accessible_Part";
     1.8 +no_document use_thys ["Accessible_Part", "Pretty_Int"];
     1.9  use_thys ["Eta", "StrongNorm"];
    1.10  if HOL_proofs < 2 then
    1.11    warning "HOL proof terms required for running theory WeakNorm"