# HG changeset patch
# User haftmann
# Date 1228550259 -3600
# Node ID d863c103ded071102139c52576e02a9e598c1a63
# Parent  d808238131e7617dfdb1ed8c64de5ae309b83e3e
adapted to changes in binding module

diff -r d808238131e7 -r d863c103ded0 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Sat Dec 06 08:45:38 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Sat Dec 06 08:57:39 2008 +0100
@@ -306,7 +306,7 @@
   a theory by constant declararion and primitive definitions:
 
   \smallskip\begin{mldecls}
-  @{ML "Sign.declare_const: Properties.T -> (Name.binding * typ) * mixfix
+  @{ML "Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix
   -> theory -> term * theory"} \\
   @{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
   \end{mldecls}
@@ -319,7 +319,7 @@
   @{ML "(fn (t, thy) => Thm.add_def false false
   (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
     (Sign.declare_const []
-      ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
+      ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
   \end{mldecls}
 
   \noindent With increasing numbers of applications, this code gets quite
@@ -333,7 +333,7 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |> (fn (t, thy) => thy
 |> Thm.add_def false false
      (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
@@ -357,7 +357,7 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |-> (fn t => Thm.add_def false false
       (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
 "}
@@ -367,7 +367,7 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Name.binding \"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 (\"bar_def\", def))
 "}
@@ -378,7 +378,7 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Name.binding \"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
       (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
@@ -390,8 +390,8 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
-||>> Sign.declare_const [] ((Name.binding \"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
       (\"bar_def\", Logic.mk_equals (t1, t2)))
 "}
@@ -437,7 +437,7 @@
 in
   thy
   |> fold_map (fn const => Sign.declare_const []
-       ((Name.binding const, @{typ \"foo => foo\"}), NoSyn)) consts
+       ((Binding.name const, @{typ \"foo => foo\"}), NoSyn)) consts
   |>> map (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
   |-> (fn defs => fold_map (fn def =>
        Thm.add_def false false (\"\", def)) defs)
@@ -475,12 +475,12 @@
   \smallskip\begin{mldecls}
 @{ML "thy
 |> tap (fn _ => writeln \"now adding constant\")
-|> Sign.declare_const [] ((Name.binding \"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 \"foobar\"))
+         (Sign.full_name thy (Binding.name \"foobar\")))
 |-> (fn (t, b) => if b then I
        else Sign.declare_const []
-         ((Name.binding \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd)
+         ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd)
 "}
   \end{mldecls}
 *}
diff -r d808238131e7 -r d863c103ded0 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Sat Dec 06 08:45:38 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Sat Dec 06 08:57:39 2008 +0100
@@ -358,7 +358,7 @@
   a theory by constant declararion and primitive definitions:
 
   \smallskip\begin{mldecls}
-  \verb|Sign.declare_const: Properties.T -> (Name.binding * typ) * mixfix|\isasep\isanewline%
+  \verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix|\isasep\isanewline%
 \verb|  -> theory -> term * theory| \\
   \verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory|
   \end{mldecls}
@@ -371,7 +371,7 @@
   \verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline%
 \verb|  ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
 \verb|    (Sign.declare_const []|\isasep\isanewline%
-\verb|      ((Name.binding "bar", @{typ "foo => foo"}), NoSyn) thy)|
+\verb|      ((Binding.name "bar", @{typ "foo => foo"}), NoSyn) thy)|
   \end{mldecls}
 
   \noindent With increasing numbers of applications, this code gets quite
@@ -386,7 +386,7 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "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|     ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
@@ -425,7 +425,7 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "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|      ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
 
@@ -435,7 +435,7 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "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 ("bar_def", def))|\isasep\isanewline%
 
@@ -446,7 +446,7 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "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|      ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
@@ -458,8 +458,8 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ((Name.binding "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|      ("bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
 
@@ -520,7 +520,7 @@
 \verb|in|\isasep\isanewline%
 \verb|  thy|\isasep\isanewline%
 \verb|  |\verb,|,\verb|> fold_map (fn const => Sign.declare_const []|\isasep\isanewline%
-\verb|       ((Name.binding const, @{typ "foo => foo"}), NoSyn)) consts|\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%
 \verb|       Thm.add_def false false ("", def)) defs)|\isasep\isanewline%
@@ -588,12 +588,12 @@
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
 \verb||\verb,|,\verb|> tap (fn _ => writeln "now adding constant")|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "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 "foobar"))|\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|         ((Name.binding "foobar", @{typ "foo => foo"}), NoSyn) #> snd)|\isasep\isanewline%
+\verb|         ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn) #> snd)|\isasep\isanewline%
 
   \end{mldecls}%
 \end{isamarkuptext}%
diff -r d808238131e7 -r d863c103ded0 doc-src/IsarImplementation/Thy/document/logic.tex
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Sat Dec 06 08:45:38 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Sat Dec 06 08:57:39 2008 +0100
@@ -3,9 +3,6 @@
 \def\isabellecontext{logic}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
@@ -328,9 +325,9 @@
   \indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
   \indexml{lambda}\verb|lambda: term -> term -> term| \\
   \indexml{betapply}\verb|betapply: term * term -> term| \\
-  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (Name.binding * typ) * mixfix ->|\isasep\isanewline%
+  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix ->|\isasep\isanewline%
 \verb|  theory -> term * theory| \\
-  \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> Name.binding * term ->|\isasep\isanewline%
+  \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> Binding.T * term ->|\isasep\isanewline%
 \verb|  theory -> (term * term) * theory| \\
   \indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
   \indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
diff -r d808238131e7 -r d863c103ded0 doc-src/IsarImplementation/Thy/document/prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Sat Dec 06 08:45:38 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Sat Dec 06 08:57:39 2008 +0100
@@ -816,13 +816,13 @@
   \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
   \indexml{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
   \indexml{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
-  \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\
+  \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> Binding.T -> string| \\
   \end{mldecls}
   \begin{mldecls}
   \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
   \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
   \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
-  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> string -> NameSpace.T -> NameSpace.T| \\
+  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T| \\
   \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
   \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
   \end{mldecls}
@@ -851,9 +851,9 @@
   \item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
   naming policy by extending its path component.
 
-  \item \verb|NameSpace.full|\isa{naming\ name} turns a name
-  specification (usually a basic name) into the fully qualified
-  internal version, according to the given naming policy.
+  \item \verb|NameSpace.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.
 
@@ -861,15 +861,16 @@
   maintaining name spaces according to theory data management
   (\secref{sec:context-data}).
 
-  \item \verb|NameSpace.declare|~\isa{naming\ name\ space} enters a
-  fully qualified name into the name space, with external accesses
-  determined by the naming policy.
+  \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|NameSpace.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| (or its derivatives for \verb|theory| and
+  names stemming from declarations are produced via \verb|NameSpace.full_name| and \verb|NameSpace.declare|
+  (or their derivatives for \verb|theory| and
   \verb|Proof.context|).
 
   \item \verb|NameSpace.extern|~\isa{space\ name} externalizes a
diff -r d808238131e7 -r d863c103ded0 doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Sat Dec 06 08:45:38 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Sat Dec 06 08:57:39 2008 +0100
@@ -1,6 +1,3 @@
-
-(* $Id$ *)
-
 theory logic imports base begin
 
 chapter {* Primitive logic \label{ch:logic} *}
@@ -326,9 +323,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 -> (Name.binding * typ) * mixfix ->
+  @{index_ML Sign.declare_const: "Properties.T -> (Binding.T * typ) * mixfix ->
   theory -> term * theory"} \\
-  @{index_ML Sign.add_abbrev: "string -> Properties.T -> Name.binding * term ->
+  @{index_ML Sign.add_abbrev: "string -> Properties.T -> Binding.T * 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"} \\
diff -r d808238131e7 -r d863c103ded0 doc-src/IsarImplementation/Thy/prelim.thy
--- a/doc-src/IsarImplementation/Thy/prelim.thy	Sat Dec 06 08:45:38 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/prelim.thy	Sat Dec 06 08:57:39 2008 +0100
@@ -707,13 +707,13 @@
   @{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: "NameSpace.naming -> string -> string"} \\
+  @{index_ML NameSpace.full_name: "NameSpace.naming -> Binding.T -> 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 -> string -> NameSpace.T -> NameSpace.T"} \\
+  @{index_ML NameSpace.declare: "NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T"} \\
   @{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\
   @{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\
   \end{mldecls}
@@ -743,9 +743,9 @@
   \item @{ML NameSpace.add_path}~@{text "path naming"} augments the
   naming policy by extending its path component.
 
-  \item @{ML NameSpace.full}@{text "naming name"} turns a name
-  specification (usually a basic name) into the fully qualified
-  internal version, according to the given naming policy.
+  \item @{ML NameSpace.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.
 
@@ -754,16 +754,17 @@
   maintaining name spaces according to theory data management
   (\secref{sec:context-data}).
 
-  \item @{ML NameSpace.declare}~@{text "naming name space"} enters a
-  fully qualified name into the name space, with external accesses
-  determined by the naming policy.
+  \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 NameSpace.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"} (or its derivatives for @{ML_type theory} and
+  "NameSpace.full_name"} and @{ML "NameSpace.declare"}
+  (or their derivatives for @{ML_type theory} and
   @{ML_type Proof.context}).
 
   \item @{ML NameSpace.extern}~@{text "space name"} externalizes a