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