doc-src/IsarImplementation/Thy/document/Prelim.tex
changeset 42401 9bfaf6819291
parent 42361 23f352990944
child 42510 b9c106763325
--- 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.