1.1 --- a/doc-src/IsarImplementation/Thy/Logic.thy	Wed Mar 28 11:04:39 2012 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/Logic.thy	Wed Mar 28 11:17:32 2012 +0200
     1.3 @@ -127,8 +127,7 @@
     1.4    \begin{mldecls}
     1.5    @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
     1.6    @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
     1.7 -  @{index_ML Sign.add_types: "Proof.context ->
     1.8 -  (binding * int * mixfix) list -> theory -> theory"} \\
     1.9 +  @{index_ML Sign.add_type: "Proof.context -> binding * int * mixfix -> theory -> theory"} \\
    1.10    @{index_ML Sign.add_type_abbrev: "Proof.context ->
    1.11    binding * string list * typ -> theory -> theory"} \\
    1.12    @{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\
    1.13 @@ -166,7 +165,7 @@
    1.14    \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type
    1.15    @{text "\<tau>"} is of sort @{text "s"}.
    1.16  
    1.17 -  \item @{ML Sign.add_types}~@{text "ctxt [(\<kappa>, k, mx), \<dots>]"} declares a
    1.18 +  \item @{ML Sign.add_type}~@{text "ctxt (\<kappa>, k, mx)"} declares a
    1.19    new type constructors @{text "\<kappa>"} with @{text "k"} arguments and
    1.20    optional mixfix syntax.
    1.21  

     2.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Wed Mar 28 11:04:39 2012 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Wed Mar 28 11:17:32 2012 +0200
     2.3 @@ -1106,8 +1106,8 @@
     2.4    @{index_ML_type Name_Space.T} \\
     2.5    @{index_ML Name_Space.empty: "string -> Name_Space.T"} \\
     2.6    @{index_ML Name_Space.merge: "Name_Space.T * Name_Space.T -> Name_Space.T"} \\
     2.7 -  @{index_ML Name_Space.declare: "Proof.context -> bool ->
     2.8 -  Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T"} \\
     2.9 +  @{index_ML Name_Space.declare: "Context.generic -> bool ->
    2.10 +  binding -> Name_Space.T -> string * Name_Space.T"} \\
    2.11    @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\
    2.12    @{index_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\
    2.13    @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"}
    2.14 @@ -1170,10 +1170,9 @@
    2.15    (\secref{sec:context-data}); @{text "kind"} is a formal comment
    2.16    to characterize the purpose of a name space.
    2.17  
    2.18 -  \item @{ML Name_Space.declare}~@{text "ctxt strict naming bindings
    2.19 +  \item @{ML Name_Space.declare}~@{text "context strict binding
    2.20    space"} enters a name binding as fully qualified internal name into
    2.21 -  the name space, with external accesses determined by the naming
    2.22 -  policy.
    2.23 +  the name space, using the naming of the context.
    2.24  
    2.25    \item @{ML Name_Space.intern}~@{text "space name"} internalizes a
    2.26    (partially qualified) external name.

     3.1 --- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Wed Mar 28 11:04:39 2012 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Wed Mar 28 11:17:32 2012 +0200
     3.3 @@ -138,8 +138,7 @@
     3.4    \begin{mldecls}
     3.5    \indexdef{}{ML}{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
     3.6    \indexdef{}{ML}{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
     3.7 -  \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: Proof.context ->|\isasep\isanewline%
     3.8 -\verb|  (binding * int * mixfix) list -> theory -> theory| \\
     3.9 +  \indexdef{}{ML}{Sign.add\_type}\verb|Sign.add_type: Proof.context -> binding * int * mixfix -> theory -> theory| \\
    3.10    \indexdef{}{ML}{Sign.add\_type\_abbrev}\verb|Sign.add_type_abbrev: Proof.context ->|\isasep\isanewline%
    3.11  \verb|  binding * string list * typ -> theory -> theory| \\
    3.12    \indexdef{}{ML}{Sign.primitive\_class}\verb|Sign.primitive_class: binding * class list -> theory -> theory| \\
    3.13 @@ -174,7 +173,7 @@
    3.14    \item \verb|Sign.of_sort|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} tests whether type
    3.15    \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is of sort \isa{s}.
    3.16  
    3.17 -  \item \verb|Sign.add_types|~\isa{ctxt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}} declares a
    3.18 +  \item \verb|Sign.add_type|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}} declares a
    3.19    new type constructors \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} with \isa{k} arguments and
    3.20    optional mixfix syntax.
    3.21  

     4.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Wed Mar 28 11:04:39 2012 +0200
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Wed Mar 28 11:17:32 2012 +0200
     4.3 @@ -1617,8 +1617,8 @@
     4.4    \indexdef{}{ML type}{Name\_Space.T}\verb|type Name_Space.T| \\
     4.5    \indexdef{}{ML}{Name\_Space.empty}\verb|Name_Space.empty: string -> Name_Space.T| \\
     4.6    \indexdef{}{ML}{Name\_Space.merge}\verb|Name_Space.merge: Name_Space.T * Name_Space.T -> Name_Space.T| \\
     4.7 -  \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: Proof.context -> bool ->|\isasep\isanewline%
     4.8 -\verb|  Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T| \\
     4.9 +  \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: Context.generic -> bool ->|\isasep\isanewline%
    4.10 +\verb|  binding -> Name_Space.T -> string * Name_Space.T| \\
    4.11    \indexdef{}{ML}{Name\_Space.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\
    4.12    \indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Proof.context -> Name_Space.T -> string -> string| \\
    4.13    \indexdef{}{ML}{Name\_Space.is\_concealed}\verb|Name_Space.is_concealed: Name_Space.T -> string -> bool|
    4.14 @@ -1677,9 +1677,8 @@
    4.15    (\secref{sec:context-data}); \isa{kind} is a formal comment
    4.16    to characterize the purpose of a name space.
    4.17  
    4.18 -  \item \verb|Name_Space.declare|~\isa{ctxt\ strict\ naming\ bindings\ space} enters a name binding as fully qualified internal name into
    4.19 -  the name space, with external accesses determined by the naming
    4.20 -  policy.
    4.21 +  \item \verb|Name_Space.declare|~\isa{context\ strict\ binding\ space} enters a name binding as fully qualified internal name into
    4.22 +  the name space, using the naming of the context.
    4.23  
    4.24    \item \verb|Name_Space.intern|~\isa{space\ name} internalizes a
    4.25    (partially qualified) external name.