src/HOL/Lambda/ROOT.ML
changeset 24994 c385c4eabb3b
parent 24535 d458d44639fc
child 25374 7657a081fcb4
--- a/src/HOL/Lambda/ROOT.ML	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Fri Oct 12 08:21:09 2007 +0200
@@ -7,7 +7,7 @@
 Syntax.ambiguity_level := 100;
 proofs := 2;
 
-no_document use_thys ["Accessible_Part", "Pretty_Int"];
+no_document use_thys ["Accessible_Part", "Code_Integer"];
 use_thys ["Eta", "StrongNorm", "Standardization"];
 if HOL_proofs < 2 then
   warning "HOL proof terms required for running theory WeakNorm"