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