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])]