merged.
authorhuffman
Sat Dec 06 23:19:44 2008 -0800 (2008-12-06)
changeset 290154546ccf72942
parent 29014 e515f42d1db7
parent 29009 3ad09b8d2534
child 29016 31110b40eae7
merged.
     1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Sat Dec 06 20:26:51 2008 -0800
     1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Sat Dec 06 23:19:44 2008 -0800
     1.3 @@ -306,7 +306,7 @@
     1.4    a theory by constant declararion and primitive definitions:
     1.5  
     1.6    \smallskip\begin{mldecls}
     1.7 -  @{ML "Sign.declare_const: Properties.T -> (Name.binding * typ) * mixfix
     1.8 +  @{ML "Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix
     1.9    -> theory -> term * theory"} \\
    1.10    @{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
    1.11    \end{mldecls}
    1.12 @@ -319,7 +319,7 @@
    1.13    @{ML "(fn (t, thy) => Thm.add_def false false
    1.14    (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
    1.15      (Sign.declare_const []
    1.16 -      ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
    1.17 +      ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
    1.18    \end{mldecls}
    1.19  
    1.20    \noindent With increasing numbers of applications, this code gets quite
    1.21 @@ -333,7 +333,7 @@
    1.22  
    1.23    \smallskip\begin{mldecls}
    1.24  @{ML "thy
    1.25 -|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
    1.26 +|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
    1.27  |> (fn (t, thy) => thy
    1.28  |> Thm.add_def false false
    1.29       (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
    1.30 @@ -357,7 +357,7 @@
    1.31  
    1.32    \smallskip\begin{mldecls}
    1.33  @{ML "thy
    1.34 -|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
    1.35 +|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
    1.36  |-> (fn t => Thm.add_def false false
    1.37        (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
    1.38  "}
    1.39 @@ -367,7 +367,7 @@
    1.40  
    1.41    \smallskip\begin{mldecls}
    1.42  @{ML "thy
    1.43 -|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
    1.44 +|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
    1.45  |>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
    1.46  |-> (fn def => Thm.add_def false false (\"bar_def\", def))
    1.47  "}
    1.48 @@ -378,7 +378,7 @@
    1.49  
    1.50    \smallskip\begin{mldecls}
    1.51  @{ML "thy
    1.52 -|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
    1.53 +|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
    1.54  ||> Sign.add_path \"foobar\"
    1.55  |-> (fn t => Thm.add_def false false
    1.56        (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
    1.57 @@ -390,8 +390,8 @@
    1.58  
    1.59    \smallskip\begin{mldecls}
    1.60  @{ML "thy
    1.61 -|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
    1.62 -||>> Sign.declare_const [] ((Name.binding \"foobar\", @{typ \"foo => foo\"}), NoSyn)
    1.63 +|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
    1.64 +||>> Sign.declare_const [] ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn)
    1.65  |-> (fn (t1, t2) => Thm.add_def false false
    1.66        (\"bar_def\", Logic.mk_equals (t1, t2)))
    1.67  "}
    1.68 @@ -437,7 +437,7 @@
    1.69  in
    1.70    thy
    1.71    |> fold_map (fn const => Sign.declare_const []
    1.72 -       ((Name.binding const, @{typ \"foo => foo\"}), NoSyn)) consts
    1.73 +       ((Binding.name const, @{typ \"foo => foo\"}), NoSyn)) consts
    1.74    |>> map (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
    1.75    |-> (fn defs => fold_map (fn def =>
    1.76         Thm.add_def false false (\"\", def)) defs)
    1.77 @@ -475,12 +475,12 @@
    1.78    \smallskip\begin{mldecls}
    1.79  @{ML "thy
    1.80  |> tap (fn _ => writeln \"now adding constant\")
    1.81 -|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
    1.82 +|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
    1.83  ||>> `(fn thy => Sign.declared_const thy
    1.84 -         (Sign.full_name thy \"foobar\"))
    1.85 +         (Sign.full_name thy (Binding.name \"foobar\")))
    1.86  |-> (fn (t, b) => if b then I
    1.87         else Sign.declare_const []
    1.88 -         ((Name.binding \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd)
    1.89 +         ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd)
    1.90  "}
    1.91    \end{mldecls}
    1.92  *}
     2.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Sat Dec 06 20:26:51 2008 -0800
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Sat Dec 06 23:19:44 2008 -0800
     2.3 @@ -358,7 +358,7 @@
     2.4    a theory by constant declararion and primitive definitions:
     2.5  
     2.6    \smallskip\begin{mldecls}
     2.7 -  \verb|Sign.declare_const: Properties.T -> (Name.binding * typ) * mixfix|\isasep\isanewline%
     2.8 +  \verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix|\isasep\isanewline%
     2.9  \verb|  -> theory -> term * theory| \\
    2.10    \verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory|
    2.11    \end{mldecls}
    2.12 @@ -371,7 +371,7 @@
    2.13    \verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline%
    2.14  \verb|  ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
    2.15  \verb|    (Sign.declare_const []|\isasep\isanewline%
    2.16 -\verb|      ((Name.binding "bar", @{typ "foo => foo"}), NoSyn) thy)|
    2.17 +\verb|      ((Binding.name "bar", @{typ "foo => foo"}), NoSyn) thy)|
    2.18    \end{mldecls}
    2.19  
    2.20    \noindent With increasing numbers of applications, this code gets quite
    2.21 @@ -386,7 +386,7 @@
    2.22  
    2.23    \smallskip\begin{mldecls}
    2.24  \verb|thy|\isasep\isanewline%
    2.25 -\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
    2.26 +\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
    2.27  \verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline%
    2.28  \verb||\verb,|,\verb|> Thm.add_def false false|\isasep\isanewline%
    2.29  \verb|     ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
    2.30 @@ -425,7 +425,7 @@
    2.31  
    2.32    \smallskip\begin{mldecls}
    2.33  \verb|thy|\isasep\isanewline%
    2.34 -\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
    2.35 +\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
    2.36  \verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
    2.37  \verb|      ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
    2.38  
    2.39 @@ -435,7 +435,7 @@
    2.40  
    2.41    \smallskip\begin{mldecls}
    2.42  \verb|thy|\isasep\isanewline%
    2.43 -\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
    2.44 +\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
    2.45  \verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
    2.46  \verb||\verb,|,\verb|-> (fn def => Thm.add_def false false ("bar_def", def))|\isasep\isanewline%
    2.47  
    2.48 @@ -446,7 +446,7 @@
    2.49  
    2.50    \smallskip\begin{mldecls}
    2.51  \verb|thy|\isasep\isanewline%
    2.52 -\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
    2.53 +\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
    2.54  \verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline%
    2.55  \verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
    2.56  \verb|      ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
    2.57 @@ -458,8 +458,8 @@
    2.58  
    2.59    \smallskip\begin{mldecls}
    2.60  \verb|thy|\isasep\isanewline%
    2.61 -\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
    2.62 -\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ((Name.binding "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
    2.63 +\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
    2.64 +\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
    2.65  \verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false false|\isasep\isanewline%
    2.66  \verb|      ("bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
    2.67  
    2.68 @@ -520,7 +520,7 @@
    2.69  \verb|in|\isasep\isanewline%
    2.70  \verb|  thy|\isasep\isanewline%
    2.71  \verb|  |\verb,|,\verb|> fold_map (fn const => Sign.declare_const []|\isasep\isanewline%
    2.72 -\verb|       ((Name.binding const, @{typ "foo => foo"}), NoSyn)) consts|\isasep\isanewline%
    2.73 +\verb|       ((Binding.name const, @{typ "foo => foo"}), NoSyn)) consts|\isasep\isanewline%
    2.74  \verb|  |\verb,|,\verb|>> map (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
    2.75  \verb|  |\verb,|,\verb|-> (fn defs => fold_map (fn def =>|\isasep\isanewline%
    2.76  \verb|       Thm.add_def false false ("", def)) defs)|\isasep\isanewline%
    2.77 @@ -588,12 +588,12 @@
    2.78    \smallskip\begin{mldecls}
    2.79  \verb|thy|\isasep\isanewline%
    2.80  \verb||\verb,|,\verb|> tap (fn _ => writeln "now adding constant")|\isasep\isanewline%
    2.81 -\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
    2.82 +\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
    2.83  \verb||\verb,|,\verb||\verb,|,\verb|>> `(fn thy => Sign.declared_const thy|\isasep\isanewline%
    2.84 -\verb|         (Sign.full_name thy "foobar"))|\isasep\isanewline%
    2.85 +\verb|         (Sign.full_name thy (Binding.name "foobar")))|\isasep\isanewline%
    2.86  \verb||\verb,|,\verb|-> (fn (t, b) => if b then I|\isasep\isanewline%
    2.87  \verb|       else Sign.declare_const []|\isasep\isanewline%
    2.88 -\verb|         ((Name.binding "foobar", @{typ "foo => foo"}), NoSyn) #> snd)|\isasep\isanewline%
    2.89 +\verb|         ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn) #> snd)|\isasep\isanewline%
    2.90  
    2.91    \end{mldecls}%
    2.92  \end{isamarkuptext}%
     3.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex	Sat Dec 06 20:26:51 2008 -0800
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Sat Dec 06 23:19:44 2008 -0800
     3.3 @@ -3,9 +3,6 @@
     3.4  \def\isabellecontext{logic}%
     3.5  %
     3.6  \isadelimtheory
     3.7 -\isanewline
     3.8 -\isanewline
     3.9 -\isanewline
    3.10  %
    3.11  \endisadelimtheory
    3.12  %
    3.13 @@ -328,9 +325,9 @@
    3.14    \indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
    3.15    \indexml{lambda}\verb|lambda: term -> term -> term| \\
    3.16    \indexml{betapply}\verb|betapply: term * term -> term| \\
    3.17 -  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (Name.binding * typ) * mixfix ->|\isasep\isanewline%
    3.18 +  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix ->|\isasep\isanewline%
    3.19  \verb|  theory -> term * theory| \\
    3.20 -  \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> Name.binding * term ->|\isasep\isanewline%
    3.21 +  \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> Binding.T * term ->|\isasep\isanewline%
    3.22  \verb|  theory -> (term * term) * theory| \\
    3.23    \indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
    3.24    \indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
     4.1 --- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Sat Dec 06 20:26:51 2008 -0800
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Sat Dec 06 23:19:44 2008 -0800
     4.3 @@ -816,13 +816,13 @@
     4.4    \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
     4.5    \indexml{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
     4.6    \indexml{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
     4.7 -  \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\
     4.8 +  \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> Binding.T -> string| \\
     4.9    \end{mldecls}
    4.10    \begin{mldecls}
    4.11    \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
    4.12    \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
    4.13    \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
    4.14 -  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> string -> NameSpace.T -> NameSpace.T| \\
    4.15 +  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T| \\
    4.16    \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
    4.17    \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
    4.18    \end{mldecls}
    4.19 @@ -851,9 +851,9 @@
    4.20    \item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
    4.21    naming policy by extending its path component.
    4.22  
    4.23 -  \item \verb|NameSpace.full|\isa{naming\ name} turns a name
    4.24 -  specification (usually a basic name) into the fully qualified
    4.25 -  internal version, according to the given naming policy.
    4.26 +  \item \verb|NameSpace.full_name|\isa{naming\ binding} turns a name
    4.27 +  binding (usually a basic name) into the fully qualified
    4.28 +  internal name, according to the given naming policy.
    4.29  
    4.30    \item \verb|NameSpace.T| represents name spaces.
    4.31  
    4.32 @@ -861,15 +861,16 @@
    4.33    maintaining name spaces according to theory data management
    4.34    (\secref{sec:context-data}).
    4.35  
    4.36 -  \item \verb|NameSpace.declare|~\isa{naming\ name\ space} enters a
    4.37 -  fully qualified name into the name space, with external accesses
    4.38 -  determined by the naming policy.
    4.39 +  \item \verb|NameSpace.declare|~\isa{naming\ bindings\ space} enters a
    4.40 +  name binding as fully qualified internal name into the name space,
    4.41 +  with external accesses determined by the naming policy.
    4.42  
    4.43    \item \verb|NameSpace.intern|~\isa{space\ name} internalizes a
    4.44    (partially qualified) external name.
    4.45  
    4.46    This operation is mostly for parsing!  Note that fully qualified
    4.47 -  names stemming from declarations are produced via \verb|NameSpace.full| (or its derivatives for \verb|theory| and
    4.48 +  names stemming from declarations are produced via \verb|NameSpace.full_name| and \verb|NameSpace.declare|
    4.49 +  (or their derivatives for \verb|theory| and
    4.50    \verb|Proof.context|).
    4.51  
    4.52    \item \verb|NameSpace.extern|~\isa{space\ name} externalizes a
     5.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Sat Dec 06 20:26:51 2008 -0800
     5.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Sat Dec 06 23:19:44 2008 -0800
     5.3 @@ -1,6 +1,3 @@
     5.4 -
     5.5 -(* $Id$ *)
     5.6 -
     5.7  theory logic imports base begin
     5.8  
     5.9  chapter {* Primitive logic \label{ch:logic} *}
    5.10 @@ -326,9 +323,9 @@
    5.11    @{index_ML fastype_of: "term -> typ"} \\
    5.12    @{index_ML lambda: "term -> term -> term"} \\
    5.13    @{index_ML betapply: "term * term -> term"} \\
    5.14 -  @{index_ML Sign.declare_const: "Properties.T -> (Name.binding * typ) * mixfix ->
    5.15 +  @{index_ML Sign.declare_const: "Properties.T -> (Binding.T * typ) * mixfix ->
    5.16    theory -> term * theory"} \\
    5.17 -  @{index_ML Sign.add_abbrev: "string -> Properties.T -> Name.binding * term ->
    5.18 +  @{index_ML Sign.add_abbrev: "string -> Properties.T -> Binding.T * term ->
    5.19    theory -> (term * term) * theory"} \\
    5.20    @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
    5.21    @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
     6.1 --- a/doc-src/IsarImplementation/Thy/prelim.thy	Sat Dec 06 20:26:51 2008 -0800
     6.2 +++ b/doc-src/IsarImplementation/Thy/prelim.thy	Sat Dec 06 23:19:44 2008 -0800
     6.3 @@ -707,13 +707,13 @@
     6.4    @{index_ML_type NameSpace.naming} \\
     6.5    @{index_ML NameSpace.default_naming: NameSpace.naming} \\
     6.6    @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
     6.7 -  @{index_ML NameSpace.full: "NameSpace.naming -> string -> string"} \\
     6.8 +  @{index_ML NameSpace.full_name: "NameSpace.naming -> Binding.T -> string"} \\
     6.9    \end{mldecls}
    6.10    \begin{mldecls}
    6.11    @{index_ML_type NameSpace.T} \\
    6.12    @{index_ML NameSpace.empty: NameSpace.T} \\
    6.13    @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
    6.14 -  @{index_ML NameSpace.declare: "NameSpace.naming -> string -> NameSpace.T -> NameSpace.T"} \\
    6.15 +  @{index_ML NameSpace.declare: "NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T"} \\
    6.16    @{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\
    6.17    @{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\
    6.18    \end{mldecls}
    6.19 @@ -743,9 +743,9 @@
    6.20    \item @{ML NameSpace.add_path}~@{text "path naming"} augments the
    6.21    naming policy by extending its path component.
    6.22  
    6.23 -  \item @{ML NameSpace.full}@{text "naming name"} turns a name
    6.24 -  specification (usually a basic name) into the fully qualified
    6.25 -  internal version, according to the given naming policy.
    6.26 +  \item @{ML NameSpace.full_name}@{text "naming binding"} turns a name
    6.27 +  binding (usually a basic name) into the fully qualified
    6.28 +  internal name, according to the given naming policy.
    6.29  
    6.30    \item @{ML_type NameSpace.T} represents name spaces.
    6.31  
    6.32 @@ -754,16 +754,17 @@
    6.33    maintaining name spaces according to theory data management
    6.34    (\secref{sec:context-data}).
    6.35  
    6.36 -  \item @{ML NameSpace.declare}~@{text "naming name space"} enters a
    6.37 -  fully qualified name into the name space, with external accesses
    6.38 -  determined by the naming policy.
    6.39 +  \item @{ML NameSpace.declare}~@{text "naming bindings space"} enters a
    6.40 +  name binding as fully qualified internal name into the name space,
    6.41 +  with external accesses determined by the naming policy.
    6.42  
    6.43    \item @{ML NameSpace.intern}~@{text "space name"} internalizes a
    6.44    (partially qualified) external name.
    6.45  
    6.46    This operation is mostly for parsing!  Note that fully qualified
    6.47    names stemming from declarations are produced via @{ML
    6.48 -  "NameSpace.full"} (or its derivatives for @{ML_type theory} and
    6.49 +  "NameSpace.full_name"} and @{ML "NameSpace.declare"}
    6.50 +  (or their derivatives for @{ML_type theory} and
    6.51    @{ML_type Proof.context}).
    6.52  
    6.53    \item @{ML NameSpace.extern}~@{text "space name"} externalizes a
     7.1 --- a/etc/settings	Sat Dec 06 20:26:51 2008 -0800
     7.2 +++ b/etc/settings	Sat Dec 06 23:19:44 2008 -0800
     7.3 @@ -75,8 +75,11 @@
     7.4  ISABELLE_SCALA="scala"
     7.5  ISABELLE_JAVA="java"
     7.6  
     7.7 -[ -e "$ISABELLE_HOME/contrib/scala" ] && \
     7.8 +if [ -e "$ISABELLE_HOME/contrib/scala" ]; then
     7.9    classpath "$ISABELLE_HOME/contrib/scala/lib/scala-library.jar"
    7.10 +elif [ -e "$ISABELLE_HOME/../scala" ]; then
    7.11 +  classpath "$ISABELLE_HOME/../scala/lib/scala-library.jar"
    7.12 +fi
    7.13  
    7.14  classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
    7.15  
    7.16 @@ -232,10 +235,22 @@
    7.17  ## Set HOME only for tools you have installed!
    7.18  
    7.19  # External provers
    7.20 -E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "/usr/local/E" "")
    7.21 -VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" \
    7.22 -  "$ISABELLE_HOME/contrib/SystemOnTPTP" "")
    7.23 -SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "/usr/local/SPASS" "")
    7.24 +E_HOME=$(choosefrom \
    7.25 +  "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" \
    7.26 +  "$ISABELLE_HOME/../E/$ML_PLATFORM" \
    7.27 +  "/usr/local/E" \
    7.28 +  "")
    7.29 +VAMPIRE_HOME=$(choosefrom \
    7.30 +  "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" \
    7.31 +  "$ISABELLE_HOME/../vampire/$ML_PLATFORM" \
    7.32 +  "/usr/local/Vampire" \
    7.33 +  "$ISABELLE_HOME/contrib/SystemOnTPTP" \
    7.34 +  "")
    7.35 +SPASS_HOME=$(choosefrom \
    7.36 +  "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" \
    7.37 +  "$ISABELLE_HOME/../spass/$ML_PLATFORM/bin" \
    7.38 +  "/usr/local/SPASS" \
    7.39 +  "")
    7.40  
    7.41  # HOL4 proof objects (cf. Isabelle/src/HOL/Import)
    7.42  #HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
     8.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sat Dec 06 20:26:51 2008 -0800
     8.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Dec 06 23:19:44 2008 -0800
     8.3 @@ -230,7 +230,7 @@
     8.4  fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy =
     8.5    let
     8.6      val (raw_eqns, atts) = split_list eqns_atts;
     8.7 -    val eqns = map (apfst Name.name_of) raw_eqns;
     8.8 +    val eqns = map (apfst Binding.base_name) raw_eqns;
     8.9      val dt_info = NominalPackage.get_nominal_datatypes thy;
    8.10      val rec_eqns = fold_rev (process_eqn thy o snd) eqns [];
    8.11      val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
     9.1 --- a/src/HOL/ROOT.ML	Sat Dec 06 20:26:51 2008 -0800
     9.2 +++ b/src/HOL/ROOT.ML	Sat Dec 06 23:19:44 2008 -0800
     9.3 @@ -3,7 +3,7 @@
     9.4  Classical Higher-order Logic -- batteries included.
     9.5  *)
     9.6  
     9.7 -use_thy "Complex/Complex_Main";
     9.8 +use_thy "Complex_Main";
     9.9  
    9.10  val HOL_proofs = ! Proofterm.proofs;
    9.11  
    10.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Sat Dec 06 20:26:51 2008 -0800
    10.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Sat Dec 06 23:19:44 2008 -0800
    10.3 @@ -82,7 +82,7 @@
    10.4                                        psimps, pinducts, termination, defname}) phi =
    10.5      let
    10.6        val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
    10.7 -      val name = Name.name_of o Morphism.binding phi o Binding.name
    10.8 +      val name = Binding.base_name o Morphism.binding phi o Binding.name
    10.9      in
   10.10        FundefCtxData { add_simps = add_simps, case_names = case_names,
   10.11                        fs = map term fs, R = term R, psimps = fact psimps, 
    11.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Dec 06 20:26:51 2008 -0800
    11.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Dec 06 23:19:44 2008 -0800
    11.3 @@ -96,8 +96,8 @@
    11.4  fun gen_add_fundef is_external prep fixspec eqnss config flags lthy =
    11.5      let
    11.6        val ((fixes0, spec0), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
    11.7 -      val fixes = map (apfst (apfst Name.name_of)) fixes0;
    11.8 -      val spec = map (apfst (apfst Name.name_of)) spec0;
    11.9 +      val fixes = map (apfst (apfst Binding.base_name)) fixes0;
   11.10 +      val spec = map (apfst (apfst Binding.base_name)) spec0;
   11.11        val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
   11.12  
   11.13        val defname = mk_defname fixes
    12.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Dec 06 20:26:51 2008 -0800
    12.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Dec 06 23:19:44 2008 -0800
    12.3 @@ -260,7 +260,7 @@
    12.4  
    12.5  fun check_rule ctxt cs params ((binding, att), rule) =
    12.6    let
    12.7 -    val name = Name.name_of binding;
    12.8 +    val err_name = Binding.display binding;
    12.9      val params' = Term.variant_frees rule (Logic.strip_params rule);
   12.10      val frees = rev (map Free params');
   12.11      val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
   12.12 @@ -278,7 +278,7 @@
   12.13  
   12.14      fun check_prem' prem t =
   12.15        if head_of t mem cs then
   12.16 -        check_ind (err_in_prem ctxt name rule prem) t
   12.17 +        check_ind (err_in_prem ctxt err_name rule prem) t
   12.18        else (case t of
   12.19            Abs (_, _, t) => check_prem' prem t
   12.20          | t $ u => (check_prem' prem t; check_prem' prem u)
   12.21 @@ -286,15 +286,15 @@
   12.22  
   12.23      fun check_prem (prem, aprem) =
   12.24        if can HOLogic.dest_Trueprop aprem then check_prem' prem prem
   12.25 -      else err_in_prem ctxt name rule prem "Non-atomic premise";
   12.26 +      else err_in_prem ctxt err_name rule prem "Non-atomic premise";
   12.27    in
   12.28      (case concl of
   12.29         Const ("Trueprop", _) $ t =>
   12.30           if head_of t mem cs then
   12.31 -           (check_ind (err_in_rule ctxt name rule') t;
   12.32 +           (check_ind (err_in_rule ctxt err_name rule') t;
   12.33              List.app check_prem (prems ~~ aprems))
   12.34 -         else err_in_rule ctxt name rule' bad_concl
   12.35 -     | _ => err_in_rule ctxt name rule' bad_concl);
   12.36 +         else err_in_rule ctxt err_name rule' bad_concl
   12.37 +     | _ => err_in_rule ctxt err_name rule' bad_concl);
   12.38      ((binding, att), arule)
   12.39    end;
   12.40  
   12.41 @@ -638,7 +638,7 @@
   12.42  
   12.43      val rec_name =
   12.44        if Binding.is_empty alt_name then
   12.45 -        Binding.name (space_implode "_" (map (Name.name_of o fst) cnames_syn))
   12.46 +        Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
   12.47        else alt_name;
   12.48  
   12.49      val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
   12.50 @@ -671,9 +671,9 @@
   12.51  fun declare_rules kind rec_binding coind no_ind cnames intrs intr_bindings intr_atts
   12.52        elims raw_induct ctxt =
   12.53    let
   12.54 -    val rec_name = Name.name_of rec_binding;
   12.55 +    val rec_name = Binding.base_name rec_binding;
   12.56      val rec_qualified = Binding.qualify rec_name;
   12.57 -    val intr_names = map Name.name_of intr_bindings;
   12.58 +    val intr_names = map Binding.base_name intr_bindings;
   12.59      val ind_case_names = RuleCases.case_names intr_names;
   12.60      val induct =
   12.61        if coind then
   12.62 @@ -730,11 +730,11 @@
   12.63      cs intros monos params cnames_syn ctxt =
   12.64    let
   12.65      val _ = null cnames_syn andalso error "No inductive predicates given";
   12.66 -    val names = map (Name.name_of o fst) cnames_syn;
   12.67 +    val names = map (Binding.base_name o fst) cnames_syn;
   12.68      val _ = message (quiet_mode andalso not verbose)
   12.69        ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
   12.70  
   12.71 -    val cnames = map (Sign.full_bname (ProofContext.theory_of ctxt) o Name.name_of o #1) cnames_syn;  (* FIXME *)
   12.72 +    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn;  (* FIXME *)
   12.73      val ((intr_names, intr_atts), intr_ts) =
   12.74        apfst split_list (split_list (map (check_rule ctxt cs params) intros));
   12.75  
   12.76 @@ -745,7 +745,7 @@
   12.77      val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
   12.78        params intr_ts rec_preds_defs ctxt1;
   12.79      val elims = if no_elim then [] else
   12.80 -      prove_elims quiet_mode cs params intr_ts (map Name.name_of intr_names)
   12.81 +      prove_elims quiet_mode cs params intr_ts (map Binding.base_name intr_names)
   12.82          unfold rec_preds_defs ctxt1;
   12.83      val raw_induct = zero_var_indexes
   12.84        (if no_ind then Drule.asm_rl else
   12.85 @@ -789,16 +789,16 @@
   12.86  
   12.87      (* abbrevs *)
   12.88  
   12.89 -    val (_, ctxt1) = Variable.add_fixes (map (Name.name_of o fst o fst) cnames_syn) lthy;
   12.90 +    val (_, ctxt1) = Variable.add_fixes (map (Binding.base_name o fst o fst) cnames_syn) lthy;
   12.91  
   12.92      fun get_abbrev ((name, atts), t) =
   12.93        if can (Logic.strip_assums_concl #> Logic.dest_equals) t then
   12.94          let
   12.95 -          val _ = Name.name_of name = "" andalso null atts orelse
   12.96 +          val _ = Binding.is_empty name andalso null atts orelse
   12.97              error "Abbreviations may not have names or attributes";
   12.98            val ((x, T), rhs) = LocalDefs.abs_def (snd (LocalDefs.cert_def ctxt1 t));
   12.99            val var =
  12.100 -            (case find_first (fn ((c, _), _) => Name.name_of c = x) cnames_syn of
  12.101 +            (case find_first (fn ((c, _), _) => Binding.base_name c = x) cnames_syn of
  12.102                NONE => error ("Undeclared head of abbreviation " ^ quote x)
  12.103              | SOME ((b, T'), mx) =>
  12.104                  if T <> T' then error ("Bad type specification for abbreviation " ^ quote x)
  12.105 @@ -807,17 +807,17 @@
  12.106        else NONE;
  12.107  
  12.108      val abbrevs = map_filter get_abbrev spec;
  12.109 -    val bs = map (Name.name_of o fst o fst) abbrevs;
  12.110 +    val bs = map (Binding.base_name o fst o fst) abbrevs;
  12.111  
  12.112  
  12.113      (* predicates *)
  12.114  
  12.115      val pre_intros = filter_out (is_some o get_abbrev) spec;
  12.116 -    val cnames_syn' = filter_out (member (op =) bs o Name.name_of o fst o fst) cnames_syn;
  12.117 -    val cs = map (Free o apfst Name.name_of o fst) cnames_syn';
  12.118 +    val cnames_syn' = filter_out (member (op =) bs o Binding.base_name o fst o fst) cnames_syn;
  12.119 +    val cs = map (Free o apfst Binding.base_name o fst) cnames_syn';
  12.120      val ps = map Free pnames;
  12.121  
  12.122 -    val (_, ctxt2) = lthy |> Variable.add_fixes (map (Name.name_of o fst o fst) cnames_syn');
  12.123 +    val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.base_name o fst o fst) cnames_syn');
  12.124      val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
  12.125      val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
  12.126      val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
  12.127 @@ -849,7 +849,7 @@
  12.128    in
  12.129      lthy
  12.130      |> LocalTheory.set_group (serial_string ())
  12.131 -    |> gen_add_inductive_i mk_def flags cs (map (apfst Name.name_of o fst) ps) intrs monos
  12.132 +    |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.base_name o fst) ps) intrs monos
  12.133    end;
  12.134  
  12.135  val add_inductive_i = gen_add_inductive_i add_ind_def;
  12.136 @@ -857,7 +857,7 @@
  12.137  
  12.138  fun add_inductive_global group flags cnames_syn pnames pre_intros monos thy =
  12.139    let
  12.140 -    val name = Sign.full_bname thy (Name.name_of (fst (fst (hd cnames_syn))));
  12.141 +    val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
  12.142      val ctxt' = thy
  12.143        |> TheoryTarget.init NONE
  12.144        |> LocalTheory.set_group group
  12.145 @@ -945,11 +945,11 @@
  12.146  fun flatten_specification specs = specs |> maps
  12.147    (fn (a, (concl, [])) => concl |> map
  12.148          (fn ((b, atts), [B]) =>
  12.149 -              if Name.name_of a = "" then ((b, atts), B)
  12.150 -              else if Name.name_of b = "" then ((a, atts), B)
  12.151 +              if Binding.is_empty a then ((b, atts), B)
  12.152 +              else if Binding.is_empty b then ((a, atts), B)
  12.153                else error "Illegal nested case names"
  12.154            | ((b, _), _) => error "Illegal simultaneous specification")
  12.155 -    | (a, _) => error ("Illegal local specification parameters for " ^ quote (Name.name_of a)));
  12.156 +    | (a, _) => error ("Illegal local specification parameters for " ^ quote (Binding.base_name a)));
  12.157  
  12.158  fun gen_ind_decl mk_def coind =
  12.159    P.fixes -- P.for_fixes --
    13.1 --- a/src/HOL/Tools/inductive_set_package.ML	Sat Dec 06 20:26:51 2008 -0800
    13.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Sat Dec 06 23:19:44 2008 -0800
    13.3 @@ -499,9 +499,9 @@
    13.4      (* convert theorems to set notation *)
    13.5      val rec_name =
    13.6        if Binding.is_empty alt_name then
    13.7 -        Binding.name (space_implode "_" (map (Name.name_of o fst) cnames_syn))
    13.8 +        Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
    13.9        else alt_name;
   13.10 -    val cnames = map (Sign.full_bname (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn;  (* FIXME *)
   13.11 +    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o #1) cnames_syn;  (* FIXME *)
   13.12      val (intr_names, intr_atts) = split_list (map fst intros);
   13.13      val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
   13.14      val (intrs', elims', induct, ctxt4) =
    14.1 --- a/src/HOL/Tools/primrec_package.ML	Sat Dec 06 20:26:51 2008 -0800
    14.2 +++ b/src/HOL/Tools/primrec_package.ML	Sat Dec 06 23:19:44 2008 -0800
    14.3 @@ -194,7 +194,7 @@
    14.4      val def_name = Thm.def_name (Sign.base_name fname);
    14.5      val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
    14.6      val SOME var = get_first (fn ((b, _), mx) =>
    14.7 -      if Name.name_of b = fname then SOME (b, mx) else NONE) fixes;
    14.8 +      if Binding.base_name b = fname then SOME (b, mx) else NONE) fixes;
    14.9    in (var, ((Binding.name def_name, []), rhs)) end;
   14.10  
   14.11  
   14.12 @@ -231,7 +231,7 @@
   14.13    let
   14.14      val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
   14.15      val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
   14.16 -      orelse exists (fn ((w, _), _) => v = Name.name_of w) fixes) o snd) spec [];
   14.17 +      orelse exists (fn ((w, _), _) => v = Binding.base_name w) fixes) o snd) spec [];
   14.18      val tnames = distinct (op =) (map (#1 o snd) eqns);
   14.19      val dts = find_dts (DatatypePackage.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
   14.20      val main_fns = map (fn (tname, {index, ...}) =>
   14.21 @@ -298,7 +298,7 @@
   14.22        P.name >> pair false) --| P.$$$ ")")) (false, "");
   14.23  
   14.24  val old_primrec_decl =
   14.25 -  opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop);
   14.26 +  opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop);
   14.27  
   14.28  fun pipe_error t = P.!!! (Scan.fail_with (K
   14.29    (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
    15.1 --- a/src/HOL/Tools/recdef_package.ML	Sat Dec 06 20:26:51 2008 -0800
    15.2 +++ b/src/HOL/Tools/recdef_package.ML	Sat Dec 06 23:19:44 2008 -0800
    15.3 @@ -299,7 +299,7 @@
    15.4  
    15.5  val recdef_decl =
    15.6    Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
    15.7 -  P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
    15.8 +  P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
    15.9      -- Scan.option hints
   15.10    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
   15.11  
   15.12 @@ -320,7 +320,7 @@
   15.13  val _ =
   15.14    OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
   15.15      K.thy_goal
   15.16 -    ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.xname --
   15.17 +    ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.xname --
   15.18          Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
   15.19        >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
   15.20  
    16.1 --- a/src/HOL/Tools/record_package.ML	Sat Dec 06 20:26:51 2008 -0800
    16.2 +++ b/src/HOL/Tools/record_package.ML	Sat Dec 06 23:19:44 2008 -0800
    16.3 @@ -346,19 +346,14 @@
    16.4  val get_updates = Symtab.lookup o #updates o get_sel_upd;
    16.5  fun get_simpset thy = Simplifier.theory_context thy (#simpset (get_sel_upd thy));
    16.6  
    16.7 -fun put_sel_upd names simps thy =
    16.8 -  let
    16.9 -    val sels = map (rpair ()) names;
   16.10 -    val upds = map (suffix updateN) names ~~ names;
   16.11 -
   16.12 -    val {records, sel_upd = {selectors, updates, simpset},
   16.13 -      equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy;
   16.14 -    val data = make_record_data records
   16.15 -      {selectors = Symtab.extend (selectors, sels),
   16.16 -        updates = Symtab.extend (updates, upds),
   16.17 -        simpset = Simplifier.addsimps (simpset, simps)}
   16.18 -       equalities extinjects extsplit splits extfields fieldext;
   16.19 -  in RecordsData.put data thy end;
   16.20 +fun put_sel_upd names simps = RecordsData.map (fn {records,
   16.21 +  sel_upd = {selectors, updates, simpset},
   16.22 +    equalities, extinjects, extsplit, splits, extfields, fieldext} =>
   16.23 +  make_record_data records
   16.24 +    {selectors = fold (fn name => Symtab.update (name, ())) names selectors,
   16.25 +      updates = fold (fn name => Symtab.update ((suffix updateN) name, name)) names updates,
   16.26 +      simpset = Simplifier.addsimps (simpset, simps)}
   16.27 +      equalities extinjects extsplit splits extfields fieldext);
   16.28  
   16.29  
   16.30  (* access 'equalities' *)
    17.1 --- a/src/HOL/Tools/refute.ML	Sat Dec 06 20:26:51 2008 -0800
    17.2 +++ b/src/HOL/Tools/refute.ML	Sat Dec 06 23:19:44 2008 -0800
    17.3 @@ -313,18 +313,10 @@
    17.4  
    17.5    (* (string * string) -> theory -> theory *)
    17.6  
    17.7 -  fun set_default_param (name, value) thy =
    17.8 -  let
    17.9 -    val {interpreters, printers, parameters} = RefuteData.get thy
   17.10 -  in
   17.11 -    RefuteData.put (case Symtab.lookup parameters name of
   17.12 -      NONE   =>
   17.13 +  fun set_default_param (name, value) = RefuteData.map 
   17.14 +    (fn {interpreters, printers, parameters} =>
   17.15        {interpreters = interpreters, printers = printers,
   17.16 -        parameters = Symtab.extend (parameters, [(name, value)])}
   17.17 -    | SOME _ =>
   17.18 -      {interpreters = interpreters, printers = printers,
   17.19 -        parameters = Symtab.update (name, value) parameters}) thy
   17.20 -  end;
   17.21 +        parameters = Symtab.update (name, value) parameters});
   17.22  
   17.23  (* ------------------------------------------------------------------------- *)
   17.24  (* get_default_param: retrieves the value associated with 'name' from        *)
    18.1 --- a/src/HOL/Tools/specification_package.ML	Sat Dec 06 20:26:51 2008 -0800
    18.2 +++ b/src/HOL/Tools/specification_package.ML	Sat Dec 06 23:19:44 2008 -0800
    18.3 @@ -233,7 +233,7 @@
    18.4  
    18.5  val specification_decl =
    18.6    P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
    18.7 -          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
    18.8 +          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
    18.9  
   18.10  val _ =
   18.11    OuterSyntax.command "specification" "define constants by specification" K.thy_goal
   18.12 @@ -244,7 +244,7 @@
   18.13  val ax_specification_decl =
   18.14      P.name --
   18.15      (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
   18.16 -           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop))
   18.17 +           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop))
   18.18  
   18.19  val _ =
   18.20    OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
    19.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Sat Dec 06 20:26:51 2008 -0800
    19.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Sat Dec 06 23:19:44 2008 -0800
    19.3 @@ -226,7 +226,7 @@
    19.4      val lengths = map length blocks;
    19.5      
    19.6      val ((bindings, srcss), strings) = apfst split_list (split_list eqns);
    19.7 -    val names = map Name.name_of bindings;
    19.8 +    val names = map Binding.base_name bindings;
    19.9      val atts = map (map (prep_attrib thy)) srcss;
   19.10      val eqn_ts = map (prep_prop thy) strings;
   19.11      val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq)))
   19.12 @@ -278,7 +278,7 @@
   19.13      val ts = map (prep_term thy) strings;
   19.14      val simps = map (fix_pat thy) ts;
   19.15    in
   19.16 -    (snd o PureThy.add_thmss [((Name.name_of name, simps), atts)]) thy
   19.17 +    (snd o PureThy.add_thmss [((Binding.base_name name, simps), atts)]) thy
   19.18    end;
   19.19  
   19.20  val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
    20.1 --- a/src/Pure/Concurrent/future.ML	Sat Dec 06 20:26:51 2008 -0800
    20.2 +++ b/src/Pure/Concurrent/future.ML	Sat Dec 06 23:19:44 2008 -0800
    20.3 @@ -36,6 +36,7 @@
    20.4    val group_of: 'a future -> group
    20.5    val peek: 'a future -> 'a Exn.result option
    20.6    val is_finished: 'a future -> bool
    20.7 +  val value: 'a -> 'a future
    20.8    val fork: (unit -> 'a) -> 'a future
    20.9    val fork_group: group -> (unit -> 'a) -> 'a future
   20.10    val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
   20.11 @@ -84,6 +85,11 @@
   20.12  fun peek (Future {result, ...}) = ! result;
   20.13  fun is_finished x = is_some (peek x);
   20.14  
   20.15 +fun value x = Future
   20.16 + {task = TaskQueue.new_task (),
   20.17 +  group = TaskQueue.new_group (),
   20.18 +  result = ref (SOME (Exn.Result x))};
   20.19 +
   20.20  
   20.21  
   20.22  (** scheduling **)
    21.1 --- a/src/Pure/Concurrent/task_queue.ML	Sat Dec 06 20:26:51 2008 -0800
    21.2 +++ b/src/Pure/Concurrent/task_queue.ML	Sat Dec 06 23:19:44 2008 -0800
    21.3 @@ -8,6 +8,7 @@
    21.4  signature TASK_QUEUE =
    21.5  sig
    21.6    eqtype task
    21.7 +  val new_task: unit -> task
    21.8    val str_of_task: task -> string
    21.9    eqtype group
   21.10    val new_group: unit -> group
   21.11 @@ -34,8 +35,11 @@
   21.12  (* identifiers *)
   21.13  
   21.14  datatype task = Task of serial;
   21.15 +fun new_task () = Task (serial ());
   21.16 +
   21.17  fun str_of_task (Task i) = string_of_int i;
   21.18  
   21.19 +
   21.20  datatype group = Group of serial * bool ref;
   21.21  
   21.22  fun new_group () = Group (serial (), ref true);
   21.23 @@ -81,8 +85,7 @@
   21.24  
   21.25  fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, focus}) =
   21.26    let
   21.27 -    val id = serial ();
   21.28 -    val task = Task id;
   21.29 +    val task as Task id = new_task ();
   21.30      val groups' = Inttab.cons_list (gid, task) groups;
   21.31      val jobs' = jobs
   21.32        |> IntGraph.new_node (id, (group, Job (pri, job))) |> fold (add_job task) deps;
    22.1 --- a/src/Pure/General/binding.ML	Sat Dec 06 20:26:51 2008 -0800
    22.2 +++ b/src/Pure/General/binding.ML	Sat Dec 06 23:19:44 2008 -0800
    22.3 @@ -23,6 +23,7 @@
    22.4    val add_prefix: bool -> string -> T -> T
    22.5    val map_prefix: ((string * bool) list -> T -> T) -> T -> T
    22.6    val is_empty: T -> bool
    22.7 +  val base_name: T -> string
    22.8    val pos_of: T -> Position.T
    22.9    val dest: T -> (string * bool) list * string
   22.10    val display: T -> string
   22.11 @@ -56,7 +57,7 @@
   22.12    else path ^ "." ^ name;
   22.13  
   22.14  val qualify = map_base o qualify_base;
   22.15 -  (*FIXME should all operations on bare names moved here from name_space.ML ?*)
   22.16 +  (*FIXME should all operations on bare names move here from name_space.ML ?*)
   22.17  
   22.18  fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
   22.19    else (map_binding o apfst) (cons (prfx, sticky)) b;
   22.20 @@ -65,6 +66,7 @@
   22.21    f prefix (name_pos (name, pos));
   22.22  
   22.23  fun is_empty (Binding ((_, name), _)) = name = "";
   22.24 +fun base_name (Binding ((_, name), _)) = name;
   22.25  fun pos_of (Binding (_, pos)) = pos;
   22.26  fun dest (Binding (prefix_name, _)) = prefix_name;
   22.27  
    23.1 --- a/src/Pure/General/name_space.ML	Sat Dec 06 20:26:51 2008 -0800
    23.2 +++ b/src/Pure/General/name_space.ML	Sat Dec 06 23:19:44 2008 -0800
    23.3 @@ -48,7 +48,6 @@
    23.4      -> 'a table * 'a table -> 'a table
    23.5    val dest_table: 'a table -> (string * 'a) list
    23.6    val extern_table: 'a table -> (xstring * 'a) list
    23.7 -  val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
    23.8  end;
    23.9  
   23.10  structure NameSpace: NAME_SPACE =
   23.11 @@ -303,10 +302,6 @@
   23.12      val (name, space') = declare naming b space;
   23.13    in (name, (space', Symtab.update_new (name, x) tab)) end;
   23.14  
   23.15 -fun extend_table naming bentries (space, tab) =
   23.16 -  let val entries = map (apfst (full_internal naming)) bentries
   23.17 -  in (fold (declare_internal naming o #1) entries space, Symtab.extend (tab, entries)) end;
   23.18 -
   23.19  fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   23.20    (merge (space1, space2), Symtab.merge eq (tab1, tab2));
   23.21  
    24.1 --- a/src/Pure/General/table.ML	Sat Dec 06 20:26:51 2008 -0800
    24.2 +++ b/src/Pure/General/table.ML	Sat Dec 06 23:19:44 2008 -0800
    24.3 @@ -41,7 +41,6 @@
    24.4    val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
    24.5    val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table
    24.6    val make: (key * 'a) list -> 'a table                                (*exception DUP*)
    24.7 -  val extend: 'a table * (key * 'a) list -> 'a table                   (*exception DUP*)
    24.8    val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
    24.9      'a table * 'a table -> 'a table                                    (*exception DUP*)
   24.10    val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUP*)
   24.11 @@ -364,9 +363,7 @@
   24.12  
   24.13  (* simultaneous modifications *)
   24.14  
   24.15 -fun extend (table, args) = fold update_new args table;
   24.16 -
   24.17 -fun make entries = extend (empty, entries);
   24.18 +fun make entries = fold update_new entries empty;
   24.19  
   24.20  fun join f (table1, table2) =
   24.21    let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
    25.1 --- a/src/Pure/Isar/attrib.ML	Sat Dec 06 20:26:51 2008 -0800
    25.2 +++ b/src/Pure/Isar/attrib.ML	Sat Dec 06 23:19:44 2008 -0800
    25.3 @@ -146,8 +146,8 @@
    25.4  fun add_attributes raw_attrs thy =
    25.5    let
    25.6      val new_attrs =
    25.7 -      raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ())));
    25.8 -    fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs
    25.9 +      raw_attrs |> map (fn (name, att, comment) => (Binding.name name, ((att, comment), stamp ())));
   25.10 +    fun add attrs = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_attrs attrs
   25.11        handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
   25.12    in Attributes.map add thy end;
   25.13  
    26.1 --- a/src/Pure/Isar/class.ML	Sat Dec 06 20:26:51 2008 -0800
    26.2 +++ b/src/Pure/Isar/class.ML	Sat Dec 06 23:19:44 2008 -0800
    26.3 @@ -545,7 +545,7 @@
    26.4      val constrain = Element.Constrains ((map o apsnd o map_atyps)
    26.5        (K (TFree (Name.aT, base_sort))) supparams);
    26.6      fun fork_syn (Element.Fixes xs) =
    26.7 -          fold_map (fn (c, ty, syn) => cons (Name.name_of c, syn) #> pair (c, ty, NoSyn)) xs
    26.8 +          fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
    26.9            #>> Element.Fixes
   26.10        | fork_syn x = pair x;
   26.11      fun fork_syntax elems =
    27.1 --- a/src/Pure/Isar/constdefs.ML	Sat Dec 06 20:26:51 2008 -0800
    27.2 +++ b/src/Pure/Isar/constdefs.ML	Sat Dec 06 23:19:44 2008 -0800
    27.3 @@ -38,7 +38,7 @@
    27.4      val prop = prep_prop var_ctxt raw_prop;
    27.5      val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
    27.6      val _ =
    27.7 -      (case Option.map Name.name_of d of
    27.8 +      (case Option.map Binding.base_name d of
    27.9          NONE => ()
   27.10        | SOME c' =>
   27.11            if c <> c' then
   27.12 @@ -46,7 +46,7 @@
   27.13            else ());
   27.14  
   27.15      val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
   27.16 -    val name = Thm.def_name_optional c (Name.name_of raw_name);
   27.17 +    val name = Thm.def_name_optional c (Binding.base_name raw_name);
   27.18      val atts = map (prep_att thy) raw_atts;
   27.19  
   27.20      val thy' =
    28.1 --- a/src/Pure/Isar/element.ML	Sat Dec 06 20:26:51 2008 -0800
    28.2 +++ b/src/Pure/Isar/element.ML	Sat Dec 06 23:19:44 2008 -0800
    28.3 @@ -113,7 +113,7 @@
    28.4    fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
    28.5         let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
    28.6     | Constrains xs => Constrains (xs |> map (fn (x, T) =>
    28.7 -       let val x' = Name.name_of (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
    28.8 +       let val x' = Binding.base_name (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
    28.9     | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
   28.10        ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
   28.11     | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
   28.12 @@ -136,7 +136,7 @@
   28.13  (* logical content *)
   28.14  
   28.15  fun params_of (Fixes fixes) = fixes |> map
   28.16 -    (fn (x, SOME T, _) => (Name.name_of x, T)
   28.17 +    (fn (x, SOME T, _) => (Binding.base_name x, T)
   28.18        | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Binding.display x), []))
   28.19    | params_of _ = [];
   28.20  
   28.21 @@ -182,8 +182,8 @@
   28.22        Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
   28.23  
   28.24      fun prt_var (x, SOME T) = Pretty.block
   28.25 -          [Pretty.str (Name.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
   28.26 -      | prt_var (x, NONE) = Pretty.str (Name.name_of x);
   28.27 +          [Pretty.str (Binding.base_name x ^ " ::"), Pretty.brk 1, prt_typ T]
   28.28 +      | prt_var (x, NONE) = Pretty.str (Binding.base_name x);
   28.29      val prt_vars = separate (Pretty.keyword "and") o map prt_var;
   28.30  
   28.31      fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
   28.32 @@ -207,9 +207,9 @@
   28.33      fun prt_mixfix NoSyn = []
   28.34        | prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx];
   28.35  
   28.36 -    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Name.name_of x ^ " ::") ::
   28.37 +    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.base_name x ^ " ::") ::
   28.38            Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
   28.39 -      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Name.name_of x) ::
   28.40 +      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.base_name x) ::
   28.41            Pretty.brk 1 :: prt_mixfix mx);
   28.42      fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
   28.43  
   28.44 @@ -395,7 +395,7 @@
   28.45  
   28.46  fun rename_var ren (b, mx) =
   28.47    let
   28.48 -    val x = Name.name_of b;
   28.49 +    val x = Binding.base_name b;
   28.50      val (x', mx') = rename_var_name ren (x, mx);
   28.51    in (Binding.name x', mx') end;
   28.52  
    29.1 --- a/src/Pure/Isar/expression.ML	Sat Dec 06 20:26:51 2008 -0800
    29.2 +++ b/src/Pure/Isar/expression.ML	Sat Dec 06 23:19:44 2008 -0800
    29.3 @@ -134,8 +134,8 @@
    29.4          if null dups then () else error (message ^ commas dups)
    29.5        end;
    29.6  
    29.7 -    fun match_bind (n, b) = (n = Name.name_of b);
    29.8 -    fun bind_eq (b1, b2) = (Name.name_of b1 = Name.name_of b2);
    29.9 +    fun match_bind (n, b) = (n = Binding.base_name b);
   29.10 +    fun bind_eq (b1, b2) = (Binding.base_name b1 = Binding.base_name b2);
   29.11        (* FIXME: cannot compare bindings for equality. *)
   29.12  
   29.13      fun params_loc loc =
   29.14 @@ -177,8 +177,8 @@
   29.15  
   29.16      val (implicit, expr') = params_expr expr;
   29.17  
   29.18 -    val implicit' = map (#1 #> Name.name_of) implicit;
   29.19 -    val fixed' = map (#1 #> Name.name_of) fixed;
   29.20 +    val implicit' = map (#1 #> Binding.base_name) implicit;
   29.21 +    val fixed' = map (#1 #> Binding.base_name) fixed;
   29.22      val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
   29.23      val implicit'' = if strict then []
   29.24        else let val _ = reject_dups
   29.25 @@ -385,7 +385,7 @@
   29.26        end;
   29.27  
   29.28  fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
   29.29 -      let val x = Name.name_of binding
   29.30 +      let val x = Binding.base_name binding
   29.31        in (binding, AList.lookup (op =) parms x, mx) end) fixes)
   29.32    | finish_primitive _ _ (Constrains _) = Constrains []
   29.33    | finish_primitive _ close (Assumes asms) = close (Assumes asms)
   29.34 @@ -396,7 +396,7 @@
   29.35    let
   29.36      val thy = ProofContext.theory_of ctxt;
   29.37      val (parm_names, parm_types) = NewLocale.params_of thy loc |>
   29.38 -      map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
   29.39 +      map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
   29.40      val (asm, defs) = NewLocale.specification_of thy loc;
   29.41      val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   29.42      val asm' = Option.map (Morphism.term morph) asm;
   29.43 @@ -440,7 +440,7 @@
   29.44      fun prep_inst (loc, (prfx, inst)) (i, insts, ctxt) =
   29.45        let
   29.46          val (parm_names, parm_types) = NewLocale.params_of thy loc |>
   29.47 -          map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
   29.48 +          map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
   29.49          val inst' = parse_inst parm_names inst ctxt;
   29.50          val parm_types' = map (TypeInfer.paramify_vars o
   29.51            Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
   29.52 @@ -473,7 +473,7 @@
   29.53      val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
   29.54  
   29.55      (* Retrieve parameter types *)
   29.56 -    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) |
   29.57 +    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.base_name o #1) fixes) |
   29.58        _ => fn ps => ps) (Fixes fors :: elems) [];
   29.59      val (Ts, ctxt') = fold_map ProofContext.inferred_param xs ctxt; 
   29.60      val parms = xs ~~ Ts;  (* params from expression and elements *)
    30.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Dec 06 20:26:51 2008 -0800
    30.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Dec 06 23:19:44 2008 -0800
    30.3 @@ -167,7 +167,7 @@
    30.4  (* axioms *)
    30.5  
    30.6  fun add_axms f args thy =
    30.7 -  f (map (fn ((b, ax), srcs) => ((Name.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy;
    30.8 +  f (map (fn ((b, ax), srcs) => ((Binding.base_name b, ax), map (Attrib.attribute thy) srcs)) args) thy;
    30.9  
   30.10  val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
   30.11  
    31.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Dec 06 20:26:51 2008 -0800
    31.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 06 23:19:44 2008 -0800
    31.3 @@ -413,7 +413,7 @@
    31.4        opt_prefix  -- SpecParse.locale_expr -- SpecParse.locale_insts
    31.5          >> (fn ((name, expr), insts) => Toplevel.print o
    31.6              Toplevel.theory_to_proof
    31.7 -              (Locale.interpretation_cmd (Name.name_of name) expr insts)));
    31.8 +              (Locale.interpretation_cmd (Binding.base_name name) expr insts)));
    31.9  
   31.10  val _ =
   31.11    OuterSyntax.command "interpret"
   31.12 @@ -422,7 +422,7 @@
   31.13      (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
   31.14        >> (fn ((name, expr), insts) => Toplevel.print o
   31.15            Toplevel.proof'
   31.16 -            (fn int => Locale.interpret_cmd (Name.name_of name) expr insts int)));
   31.17 +            (fn int => Locale.interpret_cmd (Binding.base_name name) expr insts int)));
   31.18  
   31.19  
   31.20  (* classes *)
    32.1 --- a/src/Pure/Isar/local_defs.ML	Sat Dec 06 20:26:51 2008 -0800
    32.2 +++ b/src/Pure/Isar/local_defs.ML	Sat Dec 06 23:19:44 2008 -0800
    32.3 @@ -91,7 +91,7 @@
    32.4    let
    32.5      val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
    32.6      val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
    32.7 -    val xs = map Name.name_of bvars;
    32.8 +    val xs = map Binding.base_name bvars;
    32.9      val names = map2 (Binding.map_base o Thm.def_name_optional) xs bfacts;
   32.10      val eqs = mk_def ctxt (xs ~~ rhss);
   32.11      val lhss = map (fst o Logic.dest_equals) eqs;
    33.1 --- a/src/Pure/Isar/locale.ML	Sat Dec 06 20:26:51 2008 -0800
    33.2 +++ b/src/Pure/Isar/locale.ML	Sat Dec 06 23:19:44 2008 -0800
    33.3 @@ -646,7 +646,7 @@
    33.4        | unify _ env = env;
    33.5      val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
    33.6      val Vs = map (Option.map (Envir.norm_type unifier)) Us';
    33.7 -    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
    33.8 +    val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map_filter I Vs)) unifier;
    33.9    in map (Option.map (Envir.norm_type unifier')) Vs end;
   33.10  
   33.11  fun params_of elemss =
   33.12 @@ -711,7 +711,7 @@
   33.13        (Vartab.empty, maxidx);
   33.14  
   33.15      val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
   33.16 -    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
   33.17 +    val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier;
   33.18  
   33.19      fun inst_parms (i, ps) =
   33.20        List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
   33.21 @@ -1100,15 +1100,15 @@
   33.22  *)
   33.23  
   33.24  fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
   33.25 -        val ids' = ids @ [(("", map (Name.name_of o #1) fixes), ([], Assumed []))]
   33.26 +        val ids' = ids @ [(("", map (Binding.base_name o #1) fixes), ([], Assumed []))]
   33.27        in
   33.28          ((ids',
   33.29           merge_syntax ctxt ids'
   33.30 -           (syn, Symtab.make (map (fn fx => (Name.name_of (#1 fx), #3 fx)) fixes))
   33.31 +           (syn, Symtab.make (map (fn fx => (Binding.base_name (#1 fx), #3 fx)) fixes))
   33.32             handle Symtab.DUP x => err_in_locale ctxt
   33.33               ("Conflicting syntax for parameter: " ^ quote x)
   33.34               (map #1 ids')),
   33.35 -         [((("", map (rpair NONE o Name.name_of o #1) fixes), Assumed []), Ext (Fixes fixes))])
   33.36 +         [((("", map (rpair NONE o Binding.base_name o #1) fixes), Assumed []), Ext (Fixes fixes))])
   33.37        end
   33.38    | flatten _ ((ids, syn), Elem elem) =
   33.39        ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
   33.40 @@ -1252,7 +1252,7 @@
   33.41  
   33.42  
   33.43  fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) =>
   33.44 -      let val x = Name.name_of b
   33.45 +      let val x = Binding.base_name b
   33.46        in (b, AList.lookup (op =) parms x, mx) end) fixes)
   33.47    | finish_ext_elem parms _ (Constrains _, _) = Constrains []
   33.48    | finish_ext_elem _ close (Assumes asms, propp) =
    34.1 --- a/src/Pure/Isar/method.ML	Sat Dec 06 20:26:51 2008 -0800
    34.2 +++ b/src/Pure/Isar/method.ML	Sat Dec 06 23:19:44 2008 -0800
    34.3 @@ -448,9 +448,9 @@
    34.4  fun add_methods raw_meths thy =
    34.5    let
    34.6      val new_meths = raw_meths |> map (fn (name, f, comment) =>
    34.7 -      (name, ((f, comment), stamp ())));
    34.8 +      (Binding.name name, ((f, comment), stamp ())));
    34.9  
   34.10 -    fun add meths = NameSpace.extend_table (Sign.naming_of thy) new_meths meths
   34.11 +    fun add meths = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_meths meths
   34.12        handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
   34.13    in Methods.map add thy end;
   34.14  
    35.1 --- a/src/Pure/Isar/new_locale.ML	Sat Dec 06 20:26:51 2008 -0800
    35.2 +++ b/src/Pure/Isar/new_locale.ML	Sat Dec 06 23:19:44 2008 -0800
    35.3 @@ -175,7 +175,7 @@
    35.4  
    35.5  fun instance_of thy name morph =
    35.6    params_of thy name |>
    35.7 -    map ((fn (b, T, _) => Free (Name.name_of b, the T)) #> Morphism.term morph);
    35.8 +    map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
    35.9  
   35.10  fun specification_of thy name =
   35.11    let
    36.1 --- a/src/Pure/Isar/obtain.ML	Sat Dec 06 20:26:51 2008 -0800
    36.2 +++ b/src/Pure/Isar/obtain.ML	Sat Dec 06 23:19:44 2008 -0800
    36.3 @@ -122,7 +122,7 @@
    36.4      (*obtain vars*)
    36.5      val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
    36.6      val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
    36.7 -    val xs = map (Name.name_of o #1) vars;
    36.8 +    val xs = map (Binding.base_name o #1) vars;
    36.9  
   36.10      (*obtain asms*)
   36.11      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
   36.12 @@ -261,7 +261,7 @@
   36.13  
   36.14  fun inferred_type (binding, _, mx) ctxt =
   36.15    let
   36.16 -    val x = Name.name_of binding;
   36.17 +    val x = Binding.base_name binding;
   36.18      val (T, ctxt') = ProofContext.inferred_param x ctxt
   36.19    in ((x, T, mx), ctxt') end;
   36.20  
    37.1 --- a/src/Pure/Isar/proof_context.ML	Sat Dec 06 20:26:51 2008 -0800
    37.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Dec 06 23:19:44 2008 -0800
    37.3 @@ -1012,7 +1012,7 @@
    37.4  fun prep_vars prep_typ internal =
    37.5    fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
    37.6      let
    37.7 -      val raw_x = Name.name_of raw_b;
    37.8 +      val raw_x = Binding.base_name raw_b;
    37.9        val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
   37.10        val _ = Syntax.is_identifier (no_skolem internal x) orelse
   37.11          error ("Illegal variable name: " ^ quote x);
   37.12 @@ -1122,7 +1122,7 @@
   37.13  fun gen_fixes prep raw_vars ctxt =
   37.14    let
   37.15      val (vars, _) = prep raw_vars ctxt;
   37.16 -    val (xs', ctxt') = Variable.add_fixes (map (Name.name_of o #1) vars) ctxt;
   37.17 +    val (xs', ctxt') = Variable.add_fixes (map (Binding.base_name o #1) vars) ctxt;
   37.18      val ctxt'' =
   37.19        ctxt'
   37.20        |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
    38.1 --- a/src/Pure/Isar/specification.ML	Sat Dec 06 20:26:51 2008 -0800
    38.2 +++ b/src/Pure/Isar/specification.ML	Sat Dec 06 23:19:44 2008 -0800
    38.3 @@ -153,7 +153,7 @@
    38.4  fun gen_axioms do_print prep raw_vars raw_specs thy =
    38.5    let
    38.6      val ((vars, specs), _) = prep raw_vars [raw_specs] (ProofContext.init thy);
    38.7 -    val xs = map (fn ((b, T), _) => (Name.name_of b, T)) vars;
    38.8 +    val xs = map (fn ((b, T), _) => (Binding.base_name b, T)) vars;
    38.9  
   38.10      (*consts*)
   38.11      val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
   38.12 @@ -161,7 +161,7 @@
   38.13  
   38.14      (*axioms*)
   38.15      val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
   38.16 -        fold_map Thm.add_axiom (PureThy.name_multi (Name.name_of b) (map subst props))
   38.17 +        fold_map Thm.add_axiom (PureThy.name_multi (Binding.base_name b) (map subst props))
   38.18          #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
   38.19      val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
   38.20        (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
   38.21 @@ -187,7 +187,7 @@
   38.22          [] => (Binding.name x, NoSyn)
   38.23        | [((b, _), mx)] =>
   38.24            let
   38.25 -            val y = Name.name_of b;
   38.26 +            val y = Binding.base_name b;
   38.27              val _ = x = y orelse
   38.28                error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
   38.29                  Position.str_of (Binding.pos_of b));
   38.30 @@ -220,7 +220,7 @@
   38.31          [] => (Binding.name x, NoSyn)
   38.32        | [((b, _), mx)] =>
   38.33            let
   38.34 -            val y = Name.name_of b;
   38.35 +            val y = Binding.base_name b;
   38.36              val _ = x = y orelse
   38.37                error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
   38.38                  Position.str_of (Binding.pos_of b));
   38.39 @@ -281,11 +281,11 @@
   38.40    | Element.Obtains obtains =>
   38.41        let
   38.42          val case_names = obtains |> map_index (fn (i, (b, _)) =>
   38.43 -          let val name = Name.name_of b
   38.44 +          let val name = Binding.base_name b
   38.45            in if name = "" then string_of_int (i + 1) else name end);
   38.46          val constraints = obtains |> map (fn (_, (vars, _)) =>
   38.47            Element.Constrains
   38.48 -            (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE)));
   38.49 +            (vars |> map_filter (fn (x, SOME T) => SOME (Binding.base_name x, T) | _ => NONE)));
   38.50  
   38.51          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
   38.52          val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
   38.53 @@ -295,7 +295,7 @@
   38.54          fun assume_case ((name, (vars, _)), asms) ctxt' =
   38.55            let
   38.56              val bs = map fst vars;
   38.57 -            val xs = map Name.name_of bs;
   38.58 +            val xs = map Binding.base_name bs;
   38.59              val props = map fst asms;
   38.60              val (Ts, _) = ctxt'
   38.61                |> fold Variable.declare_term props
    39.1 --- a/src/Pure/Isar/theory_target.ML	Sat Dec 06 20:26:51 2008 -0800
    39.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Dec 06 23:19:44 2008 -0800
    39.3 @@ -200,7 +200,7 @@
    39.4      val similar_body = Type.similar_types (rhs, rhs');
    39.5      (* FIXME workaround based on educated guess *)
    39.6      val (prefix', _) = Binding.dest b';
    39.7 -    val class_global = Name.name_of b = Name.name_of b'
    39.8 +    val class_global = Binding.base_name b = Binding.base_name b'
    39.9        andalso not (null prefix')
   39.10        andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
   39.11    in
   39.12 @@ -219,7 +219,7 @@
   39.13  
   39.14  fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   39.15    let
   39.16 -    val c = Name.name_of b;
   39.17 +    val c = Binding.base_name b;
   39.18      val tags = LocalTheory.group_position_of lthy;
   39.19      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
   39.20      val U = map #2 xs ---> T;
   39.21 @@ -252,7 +252,7 @@
   39.22  
   39.23  fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
   39.24    let
   39.25 -    val c = Name.name_of b;
   39.26 +    val c = Binding.base_name b;
   39.27      val tags = LocalTheory.group_position_of lthy;
   39.28      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
   39.29      val target_ctxt = LocalTheory.target_of lthy;
   39.30 @@ -289,7 +289,7 @@
   39.31      val thy = ProofContext.theory_of lthy;
   39.32      val thy_ctxt = ProofContext.init thy;
   39.33  
   39.34 -    val c = Name.name_of b;
   39.35 +    val c = Binding.base_name b;
   39.36      val name' = Binding.map_base (Thm.def_name_optional c) name;
   39.37      val (rhs', rhs_conv) =
   39.38        LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
   39.39 @@ -310,7 +310,7 @@
   39.40            then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
   39.41            else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
   39.42      val (global_def, lthy3) = lthy2
   39.43 -      |> LocalTheory.theory_result (define_const (Name.name_of name') (lhs', rhs'));
   39.44 +      |> LocalTheory.theory_result (define_const (Binding.base_name name') (lhs', rhs'));
   39.45      val def = LocalDefs.trans_terms lthy3
   39.46        [(*c == global.c xs*)     local_def,
   39.47         (*global.c xs == rhs'*)  global_def,
    40.1 --- a/src/Pure/Isar/toplevel.ML	Sat Dec 06 20:26:51 2008 -0800
    40.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Dec 06 23:19:44 2008 -0800
    40.3 @@ -744,7 +744,7 @@
    40.4      val (future_results, end_state) = fold_map (proof_result immediate) input toplevel;
    40.5      val _ =
    40.6        (case end_state of
    40.7 -        State (NONE, SOME (Theory (Context.Theory thy, _), _)) => PureThy.force_proofs thy
    40.8 +        State (NONE, SOME (Theory (Context.Theory _, _), _)) => ()
    40.9        | _ => error "Unfinished development at end of input");
   40.10      val results = maps Lazy.force future_results;
   40.11    in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end);
    41.1 --- a/src/Pure/Syntax/syntax.ML	Sat Dec 06 20:26:51 2008 -0800
    41.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Dec 06 23:19:44 2008 -0800
    41.3 @@ -173,7 +173,7 @@
    41.4  
    41.5  fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
    41.6  
    41.7 -fun update_trtab name trfuns tab = Symtab.extend (remove_trtab trfuns tab, trfuns)
    41.8 +fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
    41.9    handle Symtab.DUP c => err_dup_trfun name c;
   41.10  
   41.11  fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
    42.1 --- a/src/Pure/Thy/thy_info.ML	Sat Dec 06 20:26:51 2008 -0800
    42.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Dec 06 23:19:44 2008 -0800
    42.3 @@ -322,11 +322,22 @@
    42.4  
    42.5      fun future (name, body) tab =
    42.6        let
    42.7 -        val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
    42.8 -        val x = Future.fork_deps deps body;
    42.9 +        val deps = Graph.imm_preds task_graph name
   42.10 +          |> map_filter (fn parent =>
   42.11 +            (case Symtab.lookup tab parent of SOME future => SOME (parent, future) | NONE => NONE));
   42.12 +        fun failed (parent, future) = if can Future.join future then NONE else SOME parent;
   42.13 +
   42.14 +        val x = Future.fork_deps (map #2 deps) (fn () =>
   42.15 +          (case map_filter failed deps of
   42.16 +            [] => body ()
   42.17 +          | bad => error (loader_msg
   42.18 +              ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
   42.19 +
   42.20        in (x, Symtab.update (name, x) tab) end;
   42.21 -    val _ = ignore (Exn.release_all (Future.join_results (#1 (fold_map future tasks Symtab.empty))));
   42.22 -  in () end;
   42.23 +
   42.24 +    val thy_results = Future.join_results (#1 (fold_map future tasks Symtab.empty));
   42.25 +    val proof_results = PureThy.join_proofs (map_filter (try get_theory o #1) tasks);
   42.26 +  in ignore (Exn.release_all (thy_results @ proof_results)) end;
   42.27  
   42.28  local
   42.29  
    43.1 --- a/src/Pure/Tools/invoke.ML	Sat Dec 06 20:26:51 2008 -0800
    43.2 +++ b/src/Pure/Tools/invoke.ML	Sat Dec 06 23:19:44 2008 -0800
    43.3 @@ -120,7 +120,7 @@
    43.4      (K.tag_proof K.prf_goal)
    43.5      (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
    43.6        >> (fn ((((name, atts), expr), (insts, _)), fixes) =>
    43.7 -          Toplevel.print o Toplevel.proof' (invoke (Name.name_of name, atts) expr insts fixes)));
    43.8 +          Toplevel.print o Toplevel.proof' (invoke (Binding.base_name name, atts) expr insts fixes)));
    43.9  
   43.10  end;
   43.11  
    44.1 --- a/src/Pure/context.ML	Sat Dec 06 20:26:51 2008 -0800
    44.2 +++ b/src/Pure/context.ML	Sat Dec 06 23:19:44 2008 -0800
    44.3 @@ -1,5 +1,4 @@
    44.4  (*  Title:      Pure/context.ML
    44.5 -    ID:         $Id$
    44.6      Author:     Markus Wenzel, TU Muenchen
    44.7  
    44.8  Generic theory contexts with unique identity, arbitrarily typed data,
    44.9 @@ -392,14 +391,11 @@
   44.10  
   44.11  fun finish_thy thy = NAMED_CRITICAL "theory" (fn () =>
   44.12    let
   44.13 -    val {name, version, intermediates} = history_of thy;
   44.14 -    val rs = map ((fn TheoryRef r => r) o check_thy) intermediates;
   44.15 -    val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy;
   44.16 -    val identity' = make_identity self id ids Inttab.empty;
   44.17 +    val {name, ...} = history_of thy;
   44.18 +    val Theory (identity', data', ancestry', _) = name_thy name thy;
   44.19      val history' = make_history name 0 [];
   44.20 -    val thy'' = vitalize (Theory (identity', data', ancestry', history'));
   44.21 -    val _ = List.app (fn r => r := thy'') rs;
   44.22 -  in thy'' end);
   44.23 +    val thy' = vitalize (Theory (identity', data', ancestry', history'));
   44.24 +  in thy' end);
   44.25  
   44.26  
   44.27  (* theory data *)
    45.1 --- a/src/Pure/name.ML	Sat Dec 06 20:26:51 2008 -0800
    45.2 +++ b/src/Pure/name.ML	Sat Dec 06 23:19:44 2008 -0800
    45.3 @@ -27,8 +27,6 @@
    45.4    val variants: string list -> context -> string list * context
    45.5    val variant_list: string list -> string list -> string list
    45.6    val variant: string list -> string -> string
    45.7 -
    45.8 -  val name_of: Binding.T -> string (*FIMXE legacy*)
    45.9  end;
   45.10  
   45.11  structure Name: NAME =
   45.12 @@ -140,9 +138,4 @@
   45.13  fun variant_list used names = #1 (make_context used |> variants names);
   45.14  fun variant used = singleton (variant_list used);
   45.15  
   45.16 -
   45.17 -(** generic name bindings -- legacy **)
   45.18 -
   45.19 -val name_of = snd o Binding.dest;
   45.20 -
   45.21  end;
    46.1 --- a/src/Pure/pure_thy.ML	Sat Dec 06 20:26:51 2008 -0800
    46.2 +++ b/src/Pure/pure_thy.ML	Sat Dec 06 23:19:44 2008 -0800
    46.3 @@ -11,7 +11,7 @@
    46.4    val intern_fact: theory -> xstring -> string
    46.5    val defined_fact: theory -> string -> bool
    46.6    val hide_fact: bool -> string -> theory -> theory
    46.7 -  val force_proofs: theory -> unit
    46.8 +  val join_proofs: theory list -> unit Exn.result list
    46.9    val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   46.10    val get_thms: theory -> xstring -> thm list
   46.11    val get_thm: theory -> xstring -> thm
   46.12 @@ -79,10 +79,9 @@
   46.13  
   46.14  (* proofs *)
   46.15  
   46.16 -fun lazy_proof thm = Lazy.lazy (fn () => Thm.force_proof thm);
   46.17 +fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
   46.18  
   46.19 -fun force_proofs thy =
   46.20 -  ignore (Exn.release_all (map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy)))));
   46.21 +val join_proofs = maps (fn thy => map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy))));
   46.22  
   46.23  
   46.24  
    47.1 --- a/src/Pure/sign.ML	Sat Dec 06 20:26:51 2008 -0800
    47.2 +++ b/src/Pure/sign.ML	Sat Dec 06 23:19:44 2008 -0800
    47.3 @@ -508,10 +508,10 @@
    47.4      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
    47.5      fun prep (raw_b, raw_T, raw_mx) =
    47.6        let
    47.7 -        val (mx_name, mx) = Syntax.const_mixfix (Name.name_of raw_b) raw_mx;
    47.8 +        val (mx_name, mx) = Syntax.const_mixfix (Binding.base_name raw_b) raw_mx;
    47.9          val b = Binding.map_base (K mx_name) raw_b;
   47.10          val c = full_name thy b;
   47.11 -        val c_syn = if authentic then Syntax.constN ^ c else Name.name_of b;
   47.12 +        val c_syn = if authentic then Syntax.constN ^ c else Binding.base_name b;
   47.13          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
   47.14            cat_error msg ("in declaration of constant " ^ quote (Binding.display b));
   47.15          val T' = Logic.varifyT T;
    48.1 --- a/src/Pure/theory.ML	Sat Dec 06 20:26:51 2008 -0800
    48.2 +++ b/src/Pure/theory.ML	Sat Dec 06 23:19:44 2008 -0800
    48.3 @@ -178,8 +178,8 @@
    48.4  
    48.5  fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
    48.6    let
    48.7 -    val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
    48.8 -    val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms
    48.9 +    val axms = map (apfst Binding.name o apsnd Logic.varify o prep_axm thy) raw_axms;
   48.10 +    val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms
   48.11        handle Symtab.DUP dup => err_dup_axm dup;
   48.12    in axioms' end);
   48.13  
    49.1 --- a/src/Pure/thm.ML	Sat Dec 06 20:26:51 2008 -0800
    49.2 +++ b/src/Pure/thm.ML	Sat Dec 06 23:19:44 2008 -0800
    49.3 @@ -149,7 +149,7 @@
    49.4    val future: thm future -> cterm -> thm
    49.5    val proof_body_of: thm -> proof_body
    49.6    val proof_of: thm -> proof
    49.7 -  val force_proof: thm -> unit
    49.8 +  val join_proof: thm -> unit
    49.9    val extern_oracles: theory -> xstring list
   49.10    val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
   49.11  end;
   49.12 @@ -346,7 +346,8 @@
   49.13    tpairs: (term * term) list,                   (*flex-flex pairs*)
   49.14    prop: term}                                   (*conclusion*)
   49.15  and deriv = Deriv of
   49.16 - {all_promises: (serial * thm future) OrdList.T,
   49.17 + {max_promise: serial,
   49.18 +  open_promises: (serial * thm future) OrdList.T,
   49.19    promises: (serial * thm future) OrdList.T,
   49.20    body: Pt.proof_body};
   49.21  
   49.22 @@ -501,12 +502,11 @@
   49.23  
   49.24  (** derivations **)
   49.25  
   49.26 -fun make_deriv all_promises promises oracles thms proof =
   49.27 -  Deriv {all_promises = all_promises, promises = promises,
   49.28 +fun make_deriv max_promise open_promises promises oracles thms proof =
   49.29 +  Deriv {max_promise = max_promise, open_promises = open_promises, promises = promises,
   49.30      body = PBody {oracles = oracles, thms = thms, proof = proof}};
   49.31  
   49.32 -val closed_deriv = make_deriv [] [] [] [];
   49.33 -val empty_deriv = closed_deriv Pt.MinProof;
   49.34 +val empty_deriv = make_deriv ~1 [] [] [] [] Pt.MinProof;
   49.35  
   49.36  
   49.37  (* inference rules *)
   49.38 @@ -514,12 +514,13 @@
   49.39  fun promise_ord ((i, _), (j, _)) = int_ord (j, i);
   49.40  
   49.41  fun deriv_rule2 f
   49.42 -    (Deriv {all_promises = all_ps1, promises = ps1,
   49.43 +    (Deriv {max_promise = max1, open_promises = open_ps1, promises = ps1,
   49.44        body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
   49.45 -    (Deriv {all_promises = all_ps2, promises = ps2,
   49.46 +    (Deriv {max_promise = max2, open_promises = open_ps2, promises = ps2,
   49.47        body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
   49.48    let
   49.49 -    val all_ps = OrdList.union promise_ord all_ps1 all_ps2;
   49.50 +    val max = Int.max (max1, max2);
   49.51 +    val open_ps = OrdList.union promise_ord open_ps1 open_ps2;
   49.52      val ps = OrdList.union promise_ord ps1 ps2;
   49.53      val oras = Pt.merge_oracles oras1 oras2;
   49.54      val thms = Pt.merge_thms thms1 thms2;
   49.55 @@ -529,10 +530,10 @@
   49.56        | 1 => MinProof
   49.57        | 0 => MinProof
   49.58        | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
   49.59 -  in make_deriv all_ps ps oras thms prf end;
   49.60 +  in make_deriv max open_ps ps oras thms prf end;
   49.61  
   49.62  fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
   49.63 -fun deriv_rule0 prf = deriv_rule1 I (closed_deriv prf);
   49.64 +fun deriv_rule0 prf = deriv_rule1 I (make_deriv ~1 [] [] [] [] prf);
   49.65  
   49.66  
   49.67  
   49.68 @@ -1597,12 +1598,12 @@
   49.69      val _ = Theory.check_thy orig_thy;
   49.70      fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
   49.71  
   49.72 -    val Thm (Deriv {all_promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
   49.73 +    val Thm (Deriv {max_promise, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
   49.74      val _ = prop aconv orig_prop orelse err "bad prop";
   49.75      val _ = null tpairs orelse err "bad tpairs";
   49.76      val _ = null hyps orelse err "bad hyps";
   49.77      val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
   49.78 -    val _ = forall (fn (j, _) => j < i) all_promises orelse err "bad dependencies";
   49.79 +    val _ = max_promise < i orelse err "bad dependencies";
   49.80    in thm end;
   49.81  
   49.82  fun future future_thm ct =
   49.83 @@ -1615,7 +1616,7 @@
   49.84      val future = future_thm |> Future.map (future_result i thy sorts prop o norm_proof);
   49.85      val promise = (i, future);
   49.86    in
   49.87 -    Thm (make_deriv [promise] [promise] [] [] (Pt.promise_proof thy i prop),
   49.88 +    Thm (make_deriv i [promise] [promise] [] [] (Pt.promise_proof thy i prop),
   49.89       {thy_ref = thy_ref,
   49.90        tags = [],
   49.91        maxidx = maxidx,
   49.92 @@ -1630,14 +1631,14 @@
   49.93  
   49.94  fun raw_proof_of (Thm (Deriv {body, ...}, _)) = Proofterm.proof_of body;
   49.95  
   49.96 -fun proof_body_of (Thm (Deriv {all_promises, promises, body}, {thy_ref, ...})) =
   49.97 +fun proof_body_of (Thm (Deriv {open_promises, promises, body, ...}, {thy_ref, ...})) =
   49.98    let
   49.99 -    val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises));
  49.100 +    val _ = Exn.release_all (map (Future.join_result o #2) (rev open_promises));
  49.101      val ps = map (apsnd (raw_proof_of o Future.join)) promises;
  49.102    in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
  49.103  
  49.104  val proof_of = Proofterm.proof_of o proof_body_of;
  49.105 -val force_proof = ignore o proof_body_of;
  49.106 +val join_proof = ignore o proof_body_of;
  49.107  
  49.108  
  49.109  (* closed derivations with official name *)
  49.110 @@ -1647,14 +1648,17 @@
  49.111  
  49.112  fun put_name name (thm as Thm (der, args)) =
  49.113    let
  49.114 -    val Deriv {promises, body, ...} = der;
  49.115 +    val Deriv {max_promise, open_promises, promises, body, ...} = der;
  49.116      val {thy_ref, hyps, prop, tpairs, ...} = args;
  49.117 -    val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
  49.118 +    val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
  49.119  
  49.120      val ps = Lazy.lazy (fn () => map (apsnd (proof_of o Future.join)) promises);
  49.121      val thy = Theory.deref thy_ref;
  49.122      val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
  49.123 -    val der' = make_deriv [] [] [] [pthm] proof;
  49.124 +
  49.125 +    val open_promises' = open_promises |> filter (fn (_, p) =>
  49.126 +      (case Future.peek p of SOME (Exn.Result _) => false | _ => true));
  49.127 +    val der' = make_deriv max_promise open_promises' [] [] [pthm] proof;
  49.128      val _ = Theory.check_thy thy;
  49.129    in Thm (der', args) end;
  49.130  
  49.131 @@ -1670,7 +1674,7 @@
  49.132        raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
  49.133      else
  49.134        let val prf = Pt.oracle_proof name prop in
  49.135 -        Thm (make_deriv [] [] (Pt.make_oracles prf) [] prf,
  49.136 +        Thm (make_deriv ~1 [] [] (Pt.make_oracles prf) [] prf,
  49.137           {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
  49.138            tags = [],
  49.139            maxidx = maxidx,
    50.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Dec 06 20:26:51 2008 -0800
    50.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Dec 06 23:19:44 2008 -0800
    50.3 @@ -67,7 +67,7 @@
    50.4    val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
    50.5    val ctxt = ProofContext.init thy;
    50.6  
    50.7 -  val intr_specs = map (apfst (apfst Name.name_of)) raw_intr_specs;
    50.8 +  val intr_specs = map (apfst (apfst Binding.base_name)) raw_intr_specs;
    50.9    val (intr_names, intr_tms) = split_list (map fst intr_specs);
   50.10    val case_names = RuleCases.case_names intr_names;
   50.11  
    51.1 --- a/src/ZF/Tools/primrec_package.ML	Sat Dec 06 20:26:51 2008 -0800
    51.2 +++ b/src/ZF/Tools/primrec_package.ML	Sat Dec 06 23:19:44 2008 -0800
    51.3 @@ -180,7 +180,7 @@
    51.4  
    51.5      val (eqn_thms', thy2) =
    51.6        thy1
    51.7 -      |> PureThy.add_thms ((map Name.name_of eqn_names ~~ eqn_thms) ~~ eqn_atts);
    51.8 +      |> PureThy.add_thms ((map Binding.base_name eqn_names ~~ eqn_thms) ~~ eqn_atts);
    51.9      val (_, thy3) =
   51.10        thy2
   51.11        |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]