--- a/src/HOL/Word/ROOT.ML Tue Aug 28 03:56:24 2007 +0200 +++ b/src/HOL/Word/ROOT.ML Tue Aug 28 03:58:37 2007 +0200 @@ -1,2 +1,2 @@ no_document use_thys ["Infinite_Set", "Parity"]; -use_thy "WordExamples"; +use_thy "WordMain";