diff -r c00e04f8a52a -r 1a09f25410da src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Jun 09 14:20:09 2006 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Jun 09 16:25:05 2006 +0200
@@ -60,7 +60,7 @@
 
 time_use_thy "Refute_Examples";
 time_use_thy "Quickcheck_Examples";
-no_document time_use_thy "nbe";
+no_document time_use_thy "NormalForm";
 
 no_document use_thy "Word";
 time_use_thy "Adder";