diff -r d301ba7da9b6 -r e2bdfb2de028 src/Doc/Codegen/Inductive_Predicate.thy
--- a/src/Doc/Codegen/Inductive_Predicate.thy	Sun Feb 24 18:30:35 2013 +0100
+++ b/src/Doc/Codegen/Inductive_Predicate.thy	Sun Feb 24 20:18:32 2013 +0100
@@ -265,7 +265,7 @@
 
 text {*
   Further examples for compiling inductive predicates can be found in
-  the @{text "HOL/ex/Predicate_Compile_ex.thy"} theory file.  There are
+  the @{text "HOL/Predicate_Compile_Examples.thy"} theory file.  There are
   also some examples in the Archive of Formal Proofs, notably in the
   @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
   sessions.