diff -r 2c69bb1374b8 -r 688a8a7bcd4e src/HOL/Extraction/ROOT.ML
--- a/src/HOL/Extraction/ROOT.ML	Thu Jul 19 21:47:38 2007 +0200
+++ b/src/HOL/Extraction/ROOT.ML	Thu Jul 19 21:47:39 2007 +0200
@@ -11,5 +11,5 @@
    time_use_thy "QuotRem";
    time_use_thy "Warshall";
    time_use_thy "Higman";
-   no_document time_use_thy "EfficientNat";
+   no_document time_use_thy "Efficient_Nat";
    time_use_thy "Pigeonhole");