diff -r ac9e909fe55d -r 0a2371e7ced3 src/Doc/Codegen/Foundations.thy
--- a/src/Doc/Codegen/Foundations.thy	Fri Feb 15 08:31:30 2013 +0100
+++ b/src/Doc/Codegen/Foundations.thy	Fri Feb 15 08:31:31 2013 +0100
@@ -117,7 +117,7 @@
   interface, transforming a list of function theorems to another list
   of function theorems, provided that neither the heading constant nor
   its type change.  The @{term "0\<Colon>nat"} / @{const Suc} pattern
-  elimination implemented in theory @{text Efficient_Nat} (see
+  elimination implemented in theory @{text Code_Binary_Nat} (see
   \secref{eff_nat}) uses this interface.
 
   \noindent The current setup of the preprocessor may be inspected