diff -r 35807a5d8dc2 -r 2a1953f0d20d src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/ex/ROOT.ML	Sun Mar 25 20:15:39 2012 +0200
@@ -5,7 +5,7 @@
 
 no_document use_thys [
   "~~/src/HOL/Library/State_Monad",
-  "Efficient_Nat_examples",
+  "Code_Nat_examples",
   "~~/src/HOL/Library/FuncSet",
   "Eval_Examples",
   "Normalization_by_Evaluation",