# HG changeset patch
# User haftmann
# Date 1256543660 -3600
# Node ID 1f2051f41335e0555900a71945b6619ed3a95c97
# Parent  b8ca12f6681a0b5713d30543a58feedbdabb9e70
adjusted to changes in corresponding ML code

diff -r b8ca12f6681a -r 1f2051f41335 doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Sun Oct 25 21:35:46 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Mon Oct 26 08:54:20 2009 +0100
@@ -322,9 +322,9 @@
   @{index_ML fastype_of: "term -> typ"} \\
   @{index_ML lambda: "term -> term -> term"} \\
   @{index_ML betapply: "term * term -> term"} \\
-  @{index_ML Sign.declare_const: "Properties.T -> (binding * typ) * mixfix ->
+  @{index_ML Sign.declare_const: "(binding * typ) * mixfix ->
   theory -> term * theory"} \\
-  @{index_ML Sign.add_abbrev: "string -> Properties.T -> binding * term ->
+  @{index_ML Sign.add_abbrev: "string -> binding * term ->
   theory -> (term * term) * theory"} \\
   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
@@ -370,11 +370,11 @@
   "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
   abstraction.
 
-  \item @{ML Sign.declare_const}~@{text "properties ((c, \<sigma>), mx)"}
+  \item @{ML Sign.declare_const}~@{text "((c, \<sigma>), mx)"}
   declares a new constant @{text "c :: \<sigma>"} with optional mixfix
   syntax.
 
-  \item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"}
+  \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}
   introduces a new term abbreviation @{text "c \<equiv> t"}.
 
   \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
diff -r b8ca12f6681a -r 1f2051f41335 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Sun Oct 25 21:35:46 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Mon Oct 26 08:54:20 2009 +0100
@@ -317,7 +317,7 @@
   a theory by constant declararion and primitive definitions:
 
   \smallskip\begin{mldecls}
-  @{ML "Sign.declare_const: Properties.T -> (binding * typ) * mixfix
+  @{ML "Sign.declare_const: (binding * typ) * mixfix
   -> theory -> term * theory"} \\
   @{ML "Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory"}
   \end{mldecls}
@@ -329,7 +329,7 @@
   \smallskip\begin{mldecls}
   @{ML "(fn (t, thy) => Thm.add_def false false
   (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
-    (Sign.declare_const []
+    (Sign.declare_const
       ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
   \end{mldecls}
 
@@ -344,7 +344,7 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |> (fn (t, thy) => thy
 |> Thm.add_def false false
      (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
@@ -368,7 +368,7 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |-> (fn t => Thm.add_def false false
       (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
 "}
@@ -378,7 +378,7 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
 |-> (fn def => Thm.add_def false false (Binding.name \"bar_def\", def))
 "}
@@ -389,7 +389,7 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 ||> Sign.add_path \"foobar\"
 |-> (fn t => Thm.add_def false false
       (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
@@ -401,8 +401,8 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
-||>> Sign.declare_const [] ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+||>> Sign.declare_const ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn)
 |-> (fn (t1, t2) => Thm.add_def false false
       (Binding.name \"bar_def\", Logic.mk_equals (t1, t2)))
 "}
@@ -447,7 +447,7 @@
   val consts = [\"foo\", \"bar\"];
 in
   thy
-  |> fold_map (fn const => Sign.declare_const []
+  |> fold_map (fn const => Sign.declare_const
        ((Binding.name const, @{typ \"foo => foo\"}), NoSyn)) consts
   |>> map (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
   |-> (fn defs => fold_map (fn def =>
@@ -486,11 +486,11 @@
   \smallskip\begin{mldecls}
 @{ML "thy
 |> tap (fn _ => writeln \"now adding constant\")
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 ||>> `(fn thy => Sign.declared_const thy
          (Sign.full_name thy (Binding.name \"foobar\")))
 |-> (fn (t, b) => if b then I
-       else Sign.declare_const []
+       else Sign.declare_const
          ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd)
 "}
   \end{mldecls}
diff -r b8ca12f6681a -r 1f2051f41335 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Oct 25 21:35:46 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Mon Oct 26 08:54:20 2009 +0100
@@ -689,19 +689,19 @@
   @{index_ML Long_Name.explode: "string -> string list"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML_type NameSpace.naming} \\
-  @{index_ML NameSpace.default_naming: NameSpace.naming} \\
-  @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
-  @{index_ML NameSpace.full_name: "NameSpace.naming -> binding -> string"} \\
+  @{index_ML_type Name_Space.naming} \\
+  @{index_ML Name_Space.default_naming: Name_Space.naming} \\
+  @{index_ML Name_Space.add_path: "string -> Name_Space.naming -> Name_Space.naming"} \\
+  @{index_ML Name_Space.full_name: "Name_Space.naming -> binding -> string"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML_type NameSpace.T} \\
-  @{index_ML NameSpace.empty: NameSpace.T} \\
-  @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
-  @{index_ML NameSpace.declare: "NameSpace.naming -> binding -> NameSpace.T ->
-  string * NameSpace.T"} \\
-  @{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\
-  @{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\
+  @{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: "bool -> Name_Space.naming -> binding -> Name_Space.T ->
+  string * Name_Space.T"} \\
+  @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\
+  @{index_ML Name_Space.extern: "Name_Space.T -> string -> string"} \\
   \end{mldecls}
 
   \begin{description}
@@ -719,41 +719,43 @@
   Long_Name.explode}~@{text "name"} convert between the packed string
   representation and the explicit list form of qualified names.
 
-  \item @{ML_type NameSpace.naming} represents the abstract concept of
+  \item @{ML_type Name_Space.naming} represents the abstract concept of
   a naming policy.
 
-  \item @{ML NameSpace.default_naming} is the default naming policy.
+  \item @{ML Name_Space.default_naming} is the default naming policy.
   In a theory context, this is usually augmented by a path prefix
   consisting of the theory name.
 
-  \item @{ML NameSpace.add_path}~@{text "path naming"} augments the
+  \item @{ML Name_Space.add_path}~@{text "path naming"} augments the
   naming policy by extending its path component.
 
-  \item @{ML NameSpace.full_name}~@{text "naming binding"} turns a
+  \item @{ML Name_Space.full_name}~@{text "naming binding"} turns a
   name binding (usually a basic name) into the fully qualified
   internal name, according to the given naming policy.
 
-  \item @{ML_type NameSpace.T} represents name spaces.
+  \item @{ML_type Name_Space.T} represents name spaces.
 
-  \item @{ML NameSpace.empty} and @{ML NameSpace.merge}~@{text
+  \item @{ML Name_Space.empty}~@{text "kind"} and @{ML Name_Space.merge}~@{text
   "(space\<^isub>1, space\<^isub>2)"} are the canonical operations for
   maintaining name spaces according to theory data management
-  (\secref{sec:context-data}).
+  (\secref{sec:context-data}); @{text "kind"} is a formal comment
+  to characterize the purpose of a name space.
 
-  \item @{ML NameSpace.declare}~@{text "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 @{ML Name_Space.declare}~@{text "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 @{ML NameSpace.intern}~@{text "space name"} internalizes a
+  \item @{ML Name_Space.intern}~@{text "space name"} internalizes a
   (partially qualified) external name.
 
   This operation is mostly for parsing!  Note that fully qualified
   names stemming from declarations are produced via @{ML
-  "NameSpace.full_name"} and @{ML "NameSpace.declare"}
+  "Name_Space.full_name"} and @{ML "Name_Space.declare"}
   (or their derivatives for @{ML_type theory} and
   @{ML_type Proof.context}).
 
-  \item @{ML NameSpace.extern}~@{text "space name"} externalizes a
+  \item @{ML Name_Space.extern}~@{text "space name"} externalizes a
   (fully qualified) internal name.
 
   This operation is mostly for printing!  User code should not rely on
diff -r b8ca12f6681a -r 1f2051f41335 doc-src/IsarImplementation/Thy/document/Logic.tex
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Sun Oct 25 21:35:46 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Mon Oct 26 08:54:20 2009 +0100
@@ -325,9 +325,9 @@
   \indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\
   \indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\
   \indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\
-  \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix ->|\isasep\isanewline%
+  \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: (binding * typ) * mixfix ->|\isasep\isanewline%
 \verb|  theory -> term * theory| \\
-  \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> binding * term ->|\isasep\isanewline%
+  \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> binding * term ->|\isasep\isanewline%
 \verb|  theory -> (term * term) * theory| \\
   \indexdef{}{ML}{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
   \indexdef{}{ML}{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
@@ -365,11 +365,11 @@
   \item \verb|betapply|~\isa{{\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}} produces an application \isa{t\ u}, with topmost \isa{{\isasymbeta}}-conversion if \isa{t} is an
   abstraction.
 
-  \item \verb|Sign.declare_const|~\isa{properties\ {\isacharparenleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharparenright}{\isacharcomma}\ mx{\isacharparenright}}
+  \item \verb|Sign.declare_const|~\isa{{\isacharparenleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharparenright}{\isacharcomma}\ mx{\isacharparenright}}
   declares a new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix
   syntax.
 
-  \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ properties\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}}
+  \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}}
   introduces a new term abbreviation \isa{c\ {\isasymequiv}\ t}.
 
   \item \verb|Sign.const_typargs|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} and \verb|Sign.const_instance|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharbrackright}{\isacharparenright}}
diff -r b8ca12f6681a -r 1f2051f41335 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Sun Oct 25 21:35:46 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Mon Oct 26 08:54:20 2009 +0100
@@ -242,14 +242,14 @@
   view being presented to the user.
 
   Occasionally, such global process flags are treated like implicit
-  arguments to certain operations, by using the \verb|setmp| combinator
+  arguments to certain operations, by using the \verb|setmp_CRITICAL| combinator
   for safe temporary assignment.  Its traditional purpose was to
   ensure proper recovery of the original value when exceptions are
   raised in the body, now the functionality is extended to enter the
   \emph{critical section} (with its usual potential of degrading
   parallelism).
 
-  Note that recovery of plain value passing semantics via \verb|setmp|~\isa{ref\ value} assumes that this \isa{ref} is
+  Note that recovery of plain value passing semantics via \verb|setmp_CRITICAL|~\isa{ref\ value} assumes that this \isa{ref} is
   exclusively manipulated within the critical section.  In particular,
   any persistent global assignment of \isa{ref\ {\isacharcolon}{\isacharequal}\ value} needs to
   be marked critical as well, to prevent intruding another threads
@@ -277,7 +277,7 @@
 \begin{mldecls}
   \indexdef{}{ML}{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
   \indexdef{}{ML}{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
-  \indexdef{}{ML}{setmp}\verb|setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
+  \indexdef{}{ML}{setmp\_CRITICAL}\verb|setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
   \end{mldecls}
 
   \begin{description}
@@ -291,7 +291,7 @@
   \item \verb|CRITICAL| is the same as \verb|NAMED_CRITICAL| with empty
   name argument.
 
-  \item \verb|setmp|~\isa{ref\ value\ f\ x} evaluates \isa{f\ x}
+  \item \verb|setmp_CRITICAL|~\isa{ref\ value\ f\ x} evaluates \isa{f\ x}
   while staying within the critical section and having \isa{ref\ {\isacharcolon}{\isacharequal}\ value} assigned temporarily.  This recovers a value-passing
   semantics involving global references, regardless of exceptions or
   concurrency.
@@ -366,7 +366,7 @@
   a theory by constant declararion and primitive definitions:
 
   \smallskip\begin{mldecls}
-  \verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix|\isasep\isanewline%
+  \verb|Sign.declare_const: (binding * typ) * mixfix|\isasep\isanewline%
 \verb|  -> theory -> term * theory| \\
   \verb|Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory|
   \end{mldecls}
@@ -378,7 +378,7 @@
   \smallskip\begin{mldecls}
   \verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline%
 \verb|  (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
-\verb|    (Sign.declare_const []|\isasep\isanewline%
+\verb|    (Sign.declare_const|\isasep\isanewline%
 \verb|      ((Binding.name "bar", @{typ "foo => foo"}), NoSyn) thy)|
   \end{mldecls}
 
@@ -394,7 +394,7 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline%
 \verb||\verb,|,\verb|> Thm.add_def false false|\isasep\isanewline%
 \verb|     (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
@@ -433,7 +433,7 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
 \verb|      (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
 
@@ -443,7 +443,7 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
 \verb||\verb,|,\verb|-> (fn def => Thm.add_def false false (Binding.name "bar_def", def))|\isasep\isanewline%
 
@@ -454,7 +454,7 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline%
 \verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
 \verb|      (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
@@ -466,8 +466,8 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false false|\isasep\isanewline%
 \verb|      (Binding.name "bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
 
@@ -527,7 +527,7 @@
 \verb|  val consts = ["foo", "bar"];|\isasep\isanewline%
 \verb|in|\isasep\isanewline%
 \verb|  thy|\isasep\isanewline%
-\verb|  |\verb,|,\verb|> fold_map (fn const => Sign.declare_const []|\isasep\isanewline%
+\verb|  |\verb,|,\verb|> fold_map (fn const => Sign.declare_const|\isasep\isanewline%
 \verb|       ((Binding.name const, @{typ "foo => foo"}), NoSyn)) consts|\isasep\isanewline%
 \verb|  |\verb,|,\verb|>> map (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
 \verb|  |\verb,|,\verb|-> (fn defs => fold_map (fn def =>|\isasep\isanewline%
@@ -596,11 +596,11 @@
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
 \verb||\verb,|,\verb|> tap (fn _ => writeln "now adding constant")|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb||\verb,|,\verb|>> `(fn thy => Sign.declared_const thy|\isasep\isanewline%
 \verb|         (Sign.full_name thy (Binding.name "foobar")))|\isasep\isanewline%
 \verb||\verb,|,\verb|-> (fn (t, b) => if b then I|\isasep\isanewline%
-\verb|       else Sign.declare_const []|\isasep\isanewline%
+\verb|       else Sign.declare_const|\isasep\isanewline%
 \verb|         ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn) #> snd)|\isasep\isanewline%
 
   \end{mldecls}%
diff -r b8ca12f6681a -r 1f2051f41335 doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Oct 25 21:35:46 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Mon Oct 26 08:54:20 2009 +0100
@@ -798,19 +798,19 @@
   \indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\
   \end{mldecls}
   \begin{mldecls}
-  \indexdef{}{ML type}{NameSpace.naming}\verb|type NameSpace.naming| \\
-  \indexdef{}{ML}{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
-  \indexdef{}{ML}{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
-  \indexdef{}{ML}{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> binding -> string| \\
+  \indexdef{}{ML type}{Name\_Space.naming}\verb|type Name_Space.naming| \\
+  \indexdef{}{ML}{Name\_Space.default\_naming}\verb|Name_Space.default_naming: Name_Space.naming| \\
+  \indexdef{}{ML}{Name\_Space.add\_path}\verb|Name_Space.add_path: string -> Name_Space.naming -> Name_Space.naming| \\
+  \indexdef{}{ML}{Name\_Space.full\_name}\verb|Name_Space.full_name: Name_Space.naming -> binding -> string| \\
   \end{mldecls}
   \begin{mldecls}
-  \indexdef{}{ML type}{NameSpace.T}\verb|type NameSpace.T| \\
-  \indexdef{}{ML}{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
-  \indexdef{}{ML}{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
-  \indexdef{}{ML}{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> binding -> NameSpace.T ->|\isasep\isanewline%
-\verb|  string * NameSpace.T| \\
-  \indexdef{}{ML}{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
-  \indexdef{}{ML}{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
+  \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.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\
+  \indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Name_Space.T -> string -> string| \\
   \end{mldecls}
 
   \begin{description}
@@ -827,39 +827,40 @@
   \item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string
   representation and the explicit list form of qualified names.
 
-  \item \verb|NameSpace.naming| represents the abstract concept of
+  \item \verb|Name_Space.naming| represents the abstract concept of
   a naming policy.
 
-  \item \verb|NameSpace.default_naming| is the default naming policy.
+  \item \verb|Name_Space.default_naming| is the default naming policy.
   In a theory context, this is usually augmented by a path prefix
   consisting of the theory name.
 
-  \item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
+  \item \verb|Name_Space.add_path|~\isa{path\ naming} augments the
   naming policy by extending its path component.
 
-  \item \verb|NameSpace.full_name|~\isa{naming\ binding} turns a
+  \item \verb|Name_Space.full_name|~\isa{naming\ binding} turns a
   name binding (usually a basic name) into the fully qualified
   internal name, according to the given naming policy.
 
-  \item \verb|NameSpace.T| represents name spaces.
-
-  \item \verb|NameSpace.empty| and \verb|NameSpace.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} are the canonical operations for
-  maintaining name spaces according to theory data management
-  (\secref{sec:context-data}).
+  \item \verb|Name_Space.T| represents name spaces.
 
-  \item \verb|NameSpace.declare|~\isa{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.empty|~\isa{kind} and \verb|Name_Space.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} are the canonical operations for
+  maintaining name spaces according to theory data management
+  (\secref{sec:context-data}); \isa{kind} is a formal comment
+  to characterize the purpose of a name space.
 
-  \item \verb|NameSpace.intern|~\isa{space\ name} internalizes a
+  \item \verb|Name_Space.declare|~\isa{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.intern|~\isa{space\ name} internalizes a
   (partially qualified) external name.
 
   This operation is mostly for parsing!  Note that fully qualified
-  names stemming from declarations are produced via \verb|NameSpace.full_name| and \verb|NameSpace.declare|
+  names stemming from declarations are produced via \verb|Name_Space.full_name| and \verb|Name_Space.declare|
   (or their derivatives for \verb|theory| and
   \verb|Proof.context|).
 
-  \item \verb|NameSpace.extern|~\isa{space\ name} externalizes a
+  \item \verb|Name_Space.extern|~\isa{space\ name} externalizes a
   (fully qualified) internal name.
 
   This operation is mostly for printing!  User code should not rely on