src/HOL/Lambda/ROOT.ML

--- a/src/HOL/Lambda/ROOT.ML	Thu Apr 24 16:53:04 2008 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Fri Apr 25 15:30:33 2008 +0200
@@ -7,7 +7,7 @@
 Syntax.ambiguity_level := 100;
 Proofterm.proofs := 2;
 
-no_document use_thys ["Accessible_Part", "Code_Integer"];
+no_document use_thys ["Code_Integer"];
 use_thys ["Eta", "StrongNorm", "Standardization"];
 if HOL_proofs < 2 then
   warning "HOL proof terms required for running theory WeakNorm"