1.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Wed Mar 28 11:04:39 2012 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Wed Mar 28 11:17:32 2012 +0200
     1.3 @@ -1106,8 +1106,8 @@
     1.4    @{index_ML_type Name_Space.T} \\
     1.5    @{index_ML Name_Space.empty: "string -> Name_Space.T"} \\
     1.6    @{index_ML Name_Space.merge: "Name_Space.T * Name_Space.T -> Name_Space.T"} \\
     1.7 -  @{index_ML Name_Space.declare: "Proof.context -> bool ->
     1.8 -  Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T"} \\
     1.9 +  @{index_ML Name_Space.declare: "Context.generic -> bool ->
    1.10 +  binding -> Name_Space.T -> string * Name_Space.T"} \\
    1.11    @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\
    1.12    @{index_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\
    1.13    @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"}
    1.14 @@ -1170,10 +1170,9 @@
    1.15    (\secref{sec:context-data}); @{text "kind"} is a formal comment
    1.16    to characterize the purpose of a name space.
    1.17  
    1.18 -  \item @{ML Name_Space.declare}~@{text "ctxt strict naming bindings
    1.19 +  \item @{ML Name_Space.declare}~@{text "context strict binding
    1.20    space"} enters a name binding as fully qualified internal name into
    1.21 -  the name space, with external accesses determined by the naming
    1.22 -  policy.
    1.23 +  the name space, using the naming of the context.
    1.24  
    1.25    \item @{ML Name_Space.intern}~@{text "space name"} internalizes a
    1.26    (partially qualified) external name.