# HG changeset patch
# User wenzelm
# Date 1332926252 -7200
# Node ID b9b2e183e94d058a94db24633adbf6577a33ea33
# Parent  08d1724a63e4ec73aeda4a95ad1b28e765ed46e3
updated Sign.add_type, Name_Space.declare;

diff -r 08d1724a63e4 -r b9b2e183e94d doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Wed Mar 28 11:04:39 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Wed Mar 28 11:17:32 2012 +0200
@@ -127,8 +127,7 @@
   \begin{mldecls}
   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
-  @{index_ML Sign.add_types: "Proof.context ->
-  (binding * int * mixfix) list -> theory -> theory"} \\
+  @{index_ML Sign.add_type: "Proof.context -> binding * int * mixfix -> theory -> theory"} \\
   @{index_ML Sign.add_type_abbrev: "Proof.context ->
   binding * string list * typ -> theory -> theory"} \\
   @{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\
@@ -166,7 +165,7 @@
   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type
   @{text "\<tau>"} is of sort @{text "s"}.
 
-  \item @{ML Sign.add_types}~@{text "ctxt [(\<kappa>, k, mx), \<dots>]"} declares a
+  \item @{ML Sign.add_type}~@{text "ctxt (\<kappa>, k, mx)"} declares a
   new type constructors @{text "\<kappa>"} with @{text "k"} arguments and
   optional mixfix syntax.
 
diff -r 08d1724a63e4 -r b9b2e183e94d doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Wed Mar 28 11:04:39 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Wed Mar 28 11:17:32 2012 +0200
@@ -1106,8 +1106,8 @@
   @{index_ML_type Name_Space.T} \\
   @{index_ML Name_Space.empty: "string -> Name_Space.T"} \\
   @{index_ML Name_Space.merge: "Name_Space.T * Name_Space.T -> Name_Space.T"} \\
-  @{index_ML Name_Space.declare: "Proof.context -> bool ->
-  Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T"} \\
+  @{index_ML Name_Space.declare: "Context.generic -> bool ->
+  binding -> Name_Space.T -> string * Name_Space.T"} \\
   @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\
   @{index_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\
   @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"}
@@ -1170,10 +1170,9 @@
   (\secref{sec:context-data}); @{text "kind"} is a formal comment
   to characterize the purpose of a name space.
 
-  \item @{ML Name_Space.declare}~@{text "ctxt strict naming bindings
+  \item @{ML Name_Space.declare}~@{text "context strict binding
   space"} enters a name binding as fully qualified internal name into
-  the name space, with external accesses determined by the naming
-  policy.
+  the name space, using the naming of the context.
 
   \item @{ML Name_Space.intern}~@{text "space name"} internalizes a
   (partially qualified) external name.
diff -r 08d1724a63e4 -r b9b2e183e94d doc-src/IsarImplementation/Thy/document/Logic.tex
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Wed Mar 28 11:04:39 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Wed Mar 28 11:17:32 2012 +0200
@@ -138,8 +138,7 @@
   \begin{mldecls}
   \indexdef{}{ML}{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
   \indexdef{}{ML}{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
-  \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: Proof.context ->|\isasep\isanewline%
-\verb|  (binding * int * mixfix) list -> theory -> theory| \\
+  \indexdef{}{ML}{Sign.add\_type}\verb|Sign.add_type: Proof.context -> binding * int * mixfix -> theory -> theory| \\
   \indexdef{}{ML}{Sign.add\_type\_abbrev}\verb|Sign.add_type_abbrev: Proof.context ->|\isasep\isanewline%
 \verb|  binding * string list * typ -> theory -> theory| \\
   \indexdef{}{ML}{Sign.primitive\_class}\verb|Sign.primitive_class: binding * class list -> theory -> theory| \\
@@ -174,7 +173,7 @@
   \item \verb|Sign.of_sort|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} tests whether type
   \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is of sort \isa{s}.
 
-  \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
+  \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
   new type constructors \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} with \isa{k} arguments and
   optional mixfix syntax.
 
diff -r 08d1724a63e4 -r b9b2e183e94d doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Wed Mar 28 11:04:39 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Wed Mar 28 11:17:32 2012 +0200
@@ -1617,8 +1617,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: Proof.context -> bool ->|\isasep\isanewline%
-\verb|  Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T| \\
+  \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: Context.generic -> bool ->|\isasep\isanewline%
+\verb|  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|
@@ -1677,9 +1677,8 @@
   (\secref{sec:context-data}); \isa{kind} is a formal comment
   to characterize the purpose of a name space.
 
-  \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.
+  \item \verb|Name_Space.declare|~\isa{context\ strict\ binding\ space} enters a name binding as fully qualified internal name into
+  the name space, using the naming of the context.
 
   \item \verb|Name_Space.intern|~\isa{space\ name} internalizes a
   (partially qualified) external name.