1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Nov 13 22:05:49 2008 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Nov 13 22:06:36 2008 +0100
     1.3 @@ -309,8 +309,8 @@
     1.4    implicit in the de-Bruijn representation.  Names for bound variables
     1.5    in abstractions are maintained separately as (meaningless) comments,
     1.6    mostly for parsing and printing.  Full @{text "\<alpha>\<beta>\<eta>"}-conversion is
     1.7 -  commonplace in various standard operations (\secref{sec:rules}) that
     1.8 -  are based on higher-order unification and matching.
     1.9 +  commonplace in various standard operations (\secref{sec:obj-rules})
    1.10 +  that are based on higher-order unification and matching.
    1.11  *}
    1.12  
    1.13  text %mlref {*
    1.14 @@ -762,7 +762,7 @@
    1.15  *}
    1.16  
    1.17  
    1.18 -section {* Rules \label{sec:rules} *}
    1.19 +section {* Object-level rules \label{sec:obj-rules} *}
    1.20  
    1.21  text %FIXME {*
    1.22