1.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Tue Apr 19 10:37:38 2011 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Tue Apr 19 10:50:54 2011 +0200
     1.3 @@ -1607,8 +1607,8 @@
     1.4    \indexdef{}{ML type}{Name\_Space.T}\verb|type Name_Space.T| \\
     1.5    \indexdef{}{ML}{Name\_Space.empty}\verb|Name_Space.empty: string -> Name_Space.T| \\
     1.6    \indexdef{}{ML}{Name\_Space.merge}\verb|Name_Space.merge: Name_Space.T * Name_Space.T -> Name_Space.T| \\
     1.7 -  \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: bool -> Name_Space.naming -> binding -> Name_Space.T ->|\isasep\isanewline%
     1.8 -\verb|  string * Name_Space.T| \\
     1.9 +  \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: Proof.context -> bool ->|\isasep\isanewline%
    1.10 +\verb|  Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T| \\
    1.11    \indexdef{}{ML}{Name\_Space.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\
    1.12    \indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Proof.context -> Name_Space.T -> string -> string| \\
    1.13    \indexdef{}{ML}{Name\_Space.is\_concealed}\verb|Name_Space.is_concealed: Name_Space.T -> string -> bool|
    1.14 @@ -1667,7 +1667,7 @@
    1.15    (\secref{sec:context-data}); \isa{kind} is a formal comment
    1.16    to characterize the purpose of a name space.
    1.17  
    1.18 -  \item \verb|Name_Space.declare|~\isa{strict\ naming\ bindings\ space} enters a name binding as fully qualified internal name into
    1.19 +  \item \verb|Name_Space.declare|~\isa{ctxt\ strict\ naming\ bindings\ space} enters a name binding as fully qualified internal name into
    1.20    the name space, with external accesses determined by the naming
    1.21    policy.
    1.22