1.1 --- a/src/Doc/Functions/Functions.thy	Sun Nov 10 10:02:34 2013 +0100
     1.2 +++ b/src/Doc/Functions/Functions.thy	Sun Nov 10 15:05:06 2013 +0100
     1.3 @@ -1003,13 +1003,13 @@
     1.4    recursive calls. In general, there is one introduction rule for each
     1.5    recursive call.
     1.6  
     1.7 -  The predicate @{term "accp findzero_rel"} is the accessible part of
     1.8 +  The predicate @{term "Wellfounded.accp findzero_rel"} is the accessible part of
     1.9    that relation. An argument belongs to the accessible part, if it can
    1.10    be reached in a finite number of steps (cf.~its definition in @{text
    1.11    "Wellfounded.thy"}).
    1.12  
    1.13    Since the domain predicate is just an abbreviation, you can use
    1.14 -  lemmas for @{const accp} and @{const findzero_rel} directly. Some
    1.15 +  lemmas for @{const Wellfounded.accp} and @{const findzero_rel} directly. Some
    1.16    lemmas which are occasionally useful are @{thm [source] accpI}, @{thm [source]
    1.17    accp_downward}, and of course the introduction and elimination rules
    1.18    for the recursion relation @{thm [source] "findzero_rel.intros"} and @{thm