--- a/doc-src/IsarImplementation/Thy/Prelim.thy Mon Mar 09 09:37:33 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Mon Mar 09 10:10:34 2009 +0100
@@ -682,11 +682,11 @@
text %mlref {*
\begin{mldecls}
- @{index_ML NameSpace.base_name: "string -> string"} \\
- @{index_ML NameSpace.qualifier: "string -> string"} \\
- @{index_ML NameSpace.append: "string -> string -> string"} \\
- @{index_ML NameSpace.implode: "string list -> string"} \\
- @{index_ML NameSpace.explode: "string -> string list"} \\
+ @{index_ML Long_Name.base_name: "string -> string"} \\
+ @{index_ML Long_Name.qualifier: "string -> string"} \\
+ @{index_ML Long_Name.append: "string -> string -> string"} \\
+ @{index_ML Long_Name.implode: "string list -> string"} \\
+ @{index_ML Long_Name.explode: "string -> string list"} \\
\end{mldecls}
\begin{mldecls}
@{index_ML_type NameSpace.naming} \\
@@ -706,17 +706,17 @@
\begin{description}
- \item @{ML NameSpace.base_name}~@{text "name"} returns the base name of a
+ \item @{ML Long_Name.base_name}~@{text "name"} returns the base name of a
qualified name.
- \item @{ML NameSpace.qualifier}~@{text "name"} returns the qualifier
+ \item @{ML Long_Name.qualifier}~@{text "name"} returns the qualifier
of a qualified name.
- \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"}
+ \item @{ML Long_Name.append}~@{text "name\<^isub>1 name\<^isub>2"}
appends two qualified names.
- \item @{ML NameSpace.implode}~@{text "name"} and @{ML
- NameSpace.explode}~@{text "names"} convert between the packed string
+ \item @{ML Long_Name.implode}~@{text "names"} and @{ML
+ Long_Name.explode}~@{text "name"} convert between the packed string
representation and the explicit list form of qualified names.
\item @{ML_type NameSpace.naming} represents the abstract concept of
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon Mar 09 09:37:33 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon Mar 09 10:10:34 2009 +0100
@@ -791,11 +791,11 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{NameSpace.base\_name}\verb|NameSpace.base_name: string -> string| \\
- \indexdef{}{ML}{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
- \indexdef{}{ML}{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
- \indexdef{}{ML}{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\
- \indexdef{}{ML}{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\
+ \indexdef{}{ML}{Long\_Name.base\_name}\verb|Long_Name.base_name: string -> string| \\
+ \indexdef{}{ML}{Long\_Name.qualifier}\verb|Long_Name.qualifier: string -> string| \\
+ \indexdef{}{ML}{Long\_Name.append}\verb|Long_Name.append: string -> string -> string| \\
+ \indexdef{}{ML}{Long\_Name.implode}\verb|Long_Name.implode: string list -> string| \\
+ \indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML type}{NameSpace.naming}\verb|type NameSpace.naming| \\
@@ -815,16 +815,16 @@
\begin{description}
- \item \verb|NameSpace.base_name|~\isa{name} returns the base name of a
+ \item \verb|Long_Name.base_name|~\isa{name} returns the base name of a
qualified name.
- \item \verb|NameSpace.qualifier|~\isa{name} returns the qualifier
+ \item \verb|Long_Name.qualifier|~\isa{name} returns the qualifier
of a qualified name.
- \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
+ \item \verb|Long_Name.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
appends two qualified names.
- \item \verb|NameSpace.implode|~\isa{name} and \verb|NameSpace.explode|~\isa{names} convert between the packed string
+ \item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string
representation and the explicit list form of qualified names.
\item \verb|NameSpace.naming| represents the abstract concept of
--- a/doc-src/antiquote_setup.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/doc-src/antiquote_setup.ML Mon Mar 09 10:10:34 2009 +0100
@@ -7,9 +7,6 @@
structure AntiquoteSetup: sig end =
struct
-structure O = ThyOutput;
-
-
(* misc utils *)
fun translate f = Symbol.explode #> map f #> implode;
@@ -38,9 +35,8 @@
val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
-val _ = O.add_commands
- [("verbatim", O.args (Scan.lift Args.name) (fn _ => fn _ =>
- split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))];
+val _ = ThyOutput.antiquotation "verbatim" (fn _ => fn _ =>
+ Scan.lift Args.name >> (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
(* ML text *)
@@ -72,30 +68,30 @@
in
"\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
(txt'
- |> (if ! O.quotes then quote else I)
- |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
+ |> (if ! ThyOutput.quotes then quote else I)
+ |> (if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
end;
fun output_ml ctxt src =
- if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
+ if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
else
split_lines
#> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
#> space_implode "\\isasep\\isanewline%\n";
-fun ml_args x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
+fun ml_args x = ThyOutput.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
in
-val _ = O.add_commands
+val _ = ThyOutput.add_commands
[("index_ML", ml_args (index_ml "" ml_val)),
("index_ML_type", ml_args (index_ml "type" ml_type)),
("index_ML_exn", ml_args (index_ml "exception" ml_exn)),
("index_ML_structure", ml_args (index_ml "structure" ml_structure)),
("index_ML_functor", ml_args (index_ml "functor" ml_functor)),
- ("ML_functor", O.args (Scan.lift Args.name) output_ml),
- ("ML_text", O.args (Scan.lift Args.name) output_ml)];
+ ("ML_functor", ThyOutput.args (Scan.lift Args.name) output_ml),
+ ("ML_text", ThyOutput.args (Scan.lift Args.name) output_ml)];
end;
@@ -106,10 +102,10 @@
fun output_named_thms src ctxt xs =
map (apfst (ThyOutput.pretty_thm ctxt)) xs (*always pretty in order to exhibit errors!*)
- |> (if ! O.quotes then map (apfst Pretty.quote) else I)
- |> (if ! O.display then
+ |> (if ! ThyOutput.quotes then map (apfst Pretty.quote) else I)
+ |> (if ! ThyOutput.display then
map (fn (p, name) =>
- Output.output (Pretty.string_of (Pretty.indent (! O.indent) p)) ^
+ Output.output (Pretty.string_of (Pretty.indent (! ThyOutput.indent) p)) ^
"\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
#> space_implode "\\par\\smallskip%\n"
#> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
@@ -122,8 +118,8 @@
in
-val _ = O.add_commands
- [("named_thms", O.args (Scan.repeat (Attrib.thm --
+val _ = ThyOutput.add_commands
+ [("named_thms", ThyOutput.args (Scan.repeat (Attrib.thm --
Scan.lift (Args.parens Args.name))) output_named_thms)];
end;
@@ -131,8 +127,8 @@
(* theory files *)
-val _ = O.add_commands
- [("thy_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name =>
+val _ = ThyOutput.add_commands
+ [("thy_file", ThyOutput.args (Scan.lift Args.name) (ThyOutput.output (fn _ => fn name =>
(ThyLoad.check_thy Path.current name; Pretty.str name))))];
@@ -153,7 +149,7 @@
fun output_entity check markup index kind ctxt (logic, name) =
let
- val hyper_name = "{" ^ NameSpace.append kind (NameSpace.append logic (clean_name name)) ^ "}";
+ val hyper_name = "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
val hyper =
enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
@@ -167,14 +163,14 @@
idx ^
(Output.output name
|> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
- |> (if ! O.quotes then quote else I)
- |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+ |> (if ! ThyOutput.quotes then quote else I)
+ |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
else hyper o enclose "\\mbox{\\isa{" "}}"))
else error ("Bad " ^ kind ^ " " ^ quote name)
end;
fun entity check markup index kind =
- O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
+ ThyOutput.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
(K (output_entity check markup index kind));
fun entity_antiqs check markup kind =
@@ -184,7 +180,7 @@
in
-val _ = O.add_commands
+val _ = ThyOutput.add_commands
(entity_antiqs no_check "" "syntax" @
entity_antiqs (K (is_some o OuterKeyword.command_keyword)) "isacommand" "command" @
entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "keyword" @
--- a/src/HOL/Algebra/Ideal.thy Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Algebra/Ideal.thy Mon Mar 09 10:10:34 2009 +0100
@@ -45,7 +45,7 @@
done
qed
-subsubsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
+subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
constdefs (structure R)
genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set" ("Idl\<index> _" [80] 79)
@@ -346,8 +346,7 @@
qed
-subsection {* Ideals generated by a subset of @{term [locale=ring]
- "carrier R"} *}
+subsection (in ring) {* Ideals generated by a subset of @{term "carrier R"} *}
text {* @{term genideal} generates an ideal *}
lemma (in ring) genideal_ideal:
--- a/src/HOL/Algebra/Lattice.thy Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Algebra/Lattice.thy Mon Mar 09 10:10:34 2009 +0100
@@ -282,8 +282,8 @@
greatest :: "[_, 'a, 'a set] => bool"
"greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
-text {* Could weaken these to @{term [locale=weak_partial_order] "l \<in> carrier L \<and> l
- .\<in> A"} and @{term [locale=weak_partial_order] "g \<in> carrier L \<and> g .\<in> A"}. *}
+text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
+ .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
lemma least_closed [intro, simp]:
"least L l A ==> l \<in> carrier L"
@@ -306,8 +306,8 @@
"[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
by (unfold least_def) (auto dest: sym)
-text {* @{const least} is not congruent in the second parameter for
- @{term [locale=weak_partial_order] "A {.=} A'"} *}
+text (in weak_partial_order) {* @{const least} is not congruent in the second parameter for
+ @{term "A {.=} A'"} *}
lemma (in weak_partial_order) least_Upper_cong_l:
assumes "x .= x'"
@@ -363,8 +363,8 @@
greatest L x A = greatest L x' A"
by (unfold greatest_def) (auto dest: sym)
-text {* @{const greatest} is not congruent in the second parameter for
- @{term [locale=weak_partial_order] "A {.=} A'"} *}
+text (in weak_partial_order) {* @{const greatest} is not congruent in the second parameter for
+ @{term "A {.=} A'"} *}
lemma (in weak_partial_order) greatest_Lower_cong_l:
assumes "x .= x'"
--- a/src/HOL/Algebra/UnivPoly.thy Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Mon Mar 09 10:10:34 2009 +0100
@@ -190,7 +190,7 @@
context UP
begin
-text {*Temporarily declare @{thm [locale=UP] P_def} as simp rule.*}
+text {*Temporarily declare @{thm P_def} as simp rule.*}
declare P_def [simp]
@@ -638,8 +638,8 @@
}
qed
-text{*The following corollary follows from lemmas @{thm [locale=UP_ring] "monom_one_Suc"}
- and @{thm [locale=UP_ring] "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
+text{*The following corollary follows from lemmas @{thm "monom_one_Suc"}
+ and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
corollary monom_one_comm: shows "monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..
--- a/src/HOL/Docs/MainDoc.thy Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Docs/MainDoc.thy Mon Mar 09 10:10:34 2009 +0100
@@ -74,23 +74,22 @@
@{term"ALL x<y. P"} & @{term[source]"\<forall>x. x < y \<longrightarrow> P"}\\
@{term"ALL x>=y. P"} & @{term[source]"\<forall>x. x \<ge> y \<longrightarrow> P"}\\
@{term"ALL x>y. P"} & @{term[source]"\<forall>x. x > y \<longrightarrow> P"}\\
+\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<exists>"} instead of @{text"\<forall>"}}\\
@{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\
\end{supertabular}
-Similar for @{text"\<exists>"} instead of @{text"\<forall>"}.
-
\section{Set}
Sets are predicates: @{text[source]"'a set = 'a \<Rightarrow> bool"}
\bigskip
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
-@{const "{}"} & @{term_type_only "{}" "'a set"}\\
+@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
@{const insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\
@{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\
-@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"}\\
-@{const "op Un"} & @{term_type_only "op Un" "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"}\\
-@{const "op Int"} & @{term_type_only "op Int" "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"}\\
+@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} \qquad(\textsc{ascii} @{text":"})\\
+@{const Set.Un} & @{term_type_only Set.Un "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} \qquad(\textsc{ascii} @{text"Un"})\\
+@{const Set.Int} & @{term_type_only Set.Int "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} \qquad(\textsc{ascii} @{text"Int"})\\
@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
@{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\
@@ -112,10 +111,10 @@
@{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\
@{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\
@{term"{x. P}"} & @{term[source]"Collect(\<lambda>x. P)"}\\
-@{term"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"}\\
-@{term"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
-@{term"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"}\\
-@{term"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
+@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"}\\
+@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
+@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"}\\
+@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
@{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
@{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
@{term"range f"} & @{term[source]"f ` UNIV"}\\
@@ -345,14 +344,14 @@
\section{Set\_Interval}
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
-@{const lessThan} & @{typeof lessThan}\\
-@{const atMost} & @{typeof atMost}\\
-@{const greaterThan} & @{typeof greaterThan}\\
-@{const atLeast} & @{typeof atLeast}\\
-@{const greaterThanLessThan} & @{typeof greaterThanLessThan}\\
-@{const atLeastLessThan} & @{typeof atLeastLessThan}\\
-@{const greaterThanAtMost} & @{typeof greaterThanAtMost}\\
-@{const atLeastAtMost} & @{typeof atLeastAtMost}\\
+@{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\
+@{const atMost} & @{term_type_only atMost "'a::ord \<Rightarrow> 'a set"}\\
+@{const greaterThan} & @{term_type_only greaterThan "'a::ord \<Rightarrow> 'a set"}\\
+@{const atLeast} & @{term_type_only atLeast "'a::ord \<Rightarrow> 'a set"}\\
+@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
+@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
+@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
+@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
\end{supertabular}
\subsubsection*{Syntax}
@@ -366,8 +365,12 @@
@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\
@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\
@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\
-@{term "UN i:{..n}. A"} & @{term[source] "\<Union> i \<in> {..n}. A"}\\
+@{term[mode=xsymbols] "UN i:{..n}. A"} & @{term[source] "\<Union> i \<in> {..n}. A"}\\
+@{term[mode=xsymbols] "UN i:{..<n}. A"} & @{term[source] "\<Union> i \<in> {..<n}. A"}\\
+\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Inter>"} instead of @{text"\<Union>"}}\\
@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
+@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\
+\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\
\end{supertabular}
???????
--- a/src/HOL/Import/hol4rews.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Import/hol4rews.ML Mon Mar 09 10:10:34 2009 +0100
@@ -495,7 +495,7 @@
if internal
then
let
- val paths = NameSpace.explode isa
+ val paths = Long_Name.explode isa
val i = Library.drop(length paths - 2,paths)
in
case i of
@@ -549,10 +549,10 @@
fun gen2replay in_thy out_thy s =
let
- val ss = NameSpace.explode s
+ val ss = Long_Name.explode s
in
if (hd ss = in_thy) then
- NameSpace.implode (out_thy::(tl ss))
+ Long_Name.implode (out_thy::(tl ss))
else
s
end
--- a/src/HOL/Library/normarith.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Library/normarith.ML Mon Mar 09 10:10:34 2009 +0100
@@ -873,7 +873,7 @@
fun solve (vs,eqs) = case (vs,eqs) of
([],[]) => SOME (Intfunc.onefunc (0,Rat.one))
|(_,eq::oeqs) =>
- (case vs inter (Intfunc.dom eq) of
+ (case filter (member (op =) vs) (Intfunc.dom eq) of (*FIXME use find_first here*)
[] => NONE
| v::_ =>
if Intfunc.defined eq v
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Mon Mar 09 10:10:34 2009 +0100
@@ -72,7 +72,7 @@
let
val thy = theory_of_thm thm;
(* the parsing function returns a qualified name, we get back the base name *)
- val atom_basename = NameSpace.base_name atom_name;
+ val atom_basename = Long_Name.base_name atom_name;
val goal = List.nth(prems_of thm, i-1);
val ps = Logic.strip_params goal;
val Ts = rev (map snd ps);
@@ -159,7 +159,7 @@
NONE => all_tac thm
| SOME atom_name =>
let
- val atom_basename = NameSpace.base_name atom_name;
+ val atom_basename = Long_Name.base_name atom_name;
val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
fun inst_fresh vars params i st =
--- a/src/HOL/Nominal/nominal_inductive.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon Mar 09 10:10:34 2009 +0100
@@ -199,7 +199,7 @@
val atomTs = distinct op = (maps (map snd o #2) prems);
val ind_sort = if null atomTs then HOLogic.typeS
else Sign.certify_sort thy (map (fn T => Sign.intern_class thy
- ("fs_" ^ NameSpace.base_name (fst (dest_Type T)))) atomTs);
+ ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs);
val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
val fsT = TFree (fs_ctxt_tyname, ind_sort);
@@ -273,7 +273,7 @@
val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
val pt2_atoms = map (fn aT => PureThy.get_thm thy
- ("pt_" ^ NameSpace.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
+ ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
addsimprocs [mk_perm_bool_simproc ["Fun.id"],
@@ -281,7 +281,7 @@
val fresh_bij = PureThy.get_thms thy "fresh_bij";
val perm_bij = PureThy.get_thms thy "perm_bij";
val fs_atoms = map (fn aT => PureThy.get_thm thy
- ("fs_" ^ NameSpace.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
+ ("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
val exists_fresh' = PureThy.get_thms thy "exists_fresh'";
val fresh_atm = PureThy.get_thms thy "fresh_atm";
val swap_simps = PureThy.get_thms thy "swap_simps";
@@ -545,7 +545,7 @@
ctxt'' |>
Proof.theorem_i NONE (fn thss => fn ctxt =>
let
- val rec_name = space_implode "_" (map NameSpace.base_name names);
+ val rec_name = space_implode "_" (map Long_Name.base_name names);
val rec_qualified = Binding.qualify false rec_name;
val ind_case_names = RuleCases.case_names induct_cases;
val induct_cases' = InductivePackage.partition_rules' raw_induct
@@ -575,7 +575,7 @@
Attrib.internal (K (RuleCases.consumes 1))]),
strong_inducts) |> snd |>
LocalTheory.notes Thm.theoremK (map (fn ((name, elim), (_, cases)) =>
- ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "strong_cases"),
+ ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
[Attrib.internal (K (RuleCases.case_names (map snd cases))),
Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])]))
(strong_cases ~~ induct_cases')) |> snd
@@ -665,7 +665,7 @@
in
ctxt |>
LocalTheory.notes Thm.theoremK (map (fn (name, ths) =>
- ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "eqvt"),
+ ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
[Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
(names ~~ transp thss)) |> snd
end;
--- a/src/HOL/Nominal/nominal_inductive2.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Mar 09 10:10:34 2009 +0100
@@ -229,7 +229,7 @@
val atoms = map (fst o dest_Type) atomTs;
val ind_sort = if null atomTs then HOLogic.typeS
else Sign.certify_sort thy (map (fn a => Sign.intern_class thy
- ("fs_" ^ NameSpace.base_name a)) atoms);
+ ("fs_" ^ Long_Name.base_name a)) atoms);
val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
val fsT = TFree (fs_ctxt_tyname, ind_sort);
@@ -296,7 +296,7 @@
val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
val pt2_atoms = map (fn a => PureThy.get_thm thy
- ("pt_" ^ NameSpace.base_name a ^ "2")) atoms;
+ ("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
addsimprocs [mk_perm_bool_simproc ["Fun.id"],
@@ -324,7 +324,7 @@
val atom = fst (dest_Type T);
val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
val fs_atom = PureThy.get_thm thy
- ("fs_" ^ NameSpace.base_name atom ^ "1");
+ ("fs_" ^ Long_Name.base_name atom ^ "1");
val avoid_th = Drule.instantiate'
[SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)]
([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding});
@@ -452,7 +452,7 @@
ctxt'' |>
Proof.theorem_i NONE (fn thss => fn ctxt =>
let
- val rec_name = space_implode "_" (map NameSpace.base_name names);
+ val rec_name = space_implode "_" (map Long_Name.base_name names);
val rec_qualified = Binding.qualify false rec_name;
val ind_case_names = RuleCases.case_names induct_cases;
val induct_cases' = InductivePackage.partition_rules' raw_induct
--- a/src/HOL/Nominal/nominal_package.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Nominal/nominal_package.ML Mon Mar 09 10:10:34 2009 +0100
@@ -49,9 +49,9 @@
fun dt_cases (descr: descr) (_, args, constrs) =
let
- fun the_bname i = NameSpace.base_name (#1 (valOf (AList.lookup (op =) descr i)));
+ fun the_bname i = Long_Name.base_name (#1 (valOf (AList.lookup (op =) descr i)));
val bnames = map the_bname (distinct op = (List.concat (map dt_recs args)));
- in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end;
+ in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
fun induct_cases descr =
@@ -364,7 +364,7 @@
val pi2 = Free ("pi2", permT);
val pt_inst = pt_inst_of thy2 a;
val pt2' = pt_inst RS pt2;
- val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base_name (fn s => "pt_" ^ s ^ "2") a);
+ val pt2_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
in List.take (map standard (split_conj_thm
(Goal.prove_global thy2 [] []
(augment_sort thy2 [pt_class_of thy2 a]
@@ -399,7 +399,7 @@
val pt_inst = pt_inst_of thy2 a;
val pt3' = pt_inst RS pt3;
val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
- val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base_name (fn s => "pt_" ^ s ^ "3") a);
+ val pt3_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
in List.take (map standard (split_conj_thm
(Goal.prove_global thy2 [] []
(augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
@@ -665,7 +665,7 @@
asm_full_simp_tac (simpset_of thy addsimps
[Rep RS perm_closed RS Abs_inverse]) 1,
asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
- ("pt_" ^ NameSpace.base_name atom ^ "3")]) 1]) thy
+ ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy
end)
(Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
new_type_names ~~ tyvars ~~ perm_closed_thms);
@@ -729,8 +729,8 @@
(** strips the "_Rep" in type names *)
fun strip_nth_name i s =
- let val xs = NameSpace.explode s;
- in NameSpace.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
+ let val xs = Long_Name.explode s;
+ in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
val (descr'', ndescr) = ListPair.unzip (List.mapPartial
(fn (i, ("Nominal.noption", _, _)) => NONE
@@ -799,7 +799,7 @@
val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
(Const (rep_name, T --> T') $ lhs, rhs));
- val def_name = (NameSpace.base_name cname) ^ "_def";
+ val def_name = (Long_Name.base_name cname) ^ "_def";
val ([def_thm], thy') = thy |>
Sign.add_consts_i [(Binding.name cname', constrT, mx)] |>
(PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
@@ -890,7 +890,7 @@
map (fn ((cname, dts), constr_rep_thm) =>
let
val cname = Sign.intern_const thy8
- (NameSpace.append tname (NameSpace.base_name cname));
+ (Long_Name.append tname (Long_Name.base_name cname));
val permT = mk_permT (Type (atom, []));
val pi = Free ("pi", permT);
@@ -946,7 +946,7 @@
if null dts then NONE else SOME
let
val cname = Sign.intern_const thy8
- (NameSpace.append tname (NameSpace.base_name cname));
+ (Long_Name.append tname (Long_Name.base_name cname));
fun make_inj ((dts, dt), (j, args1, args2, eqs)) =
let
@@ -988,7 +988,7 @@
in List.concat (map (fn (cname, dts) => map (fn atom =>
let
val cname = Sign.intern_const thy8
- (NameSpace.append tname (NameSpace.base_name cname));
+ (Long_Name.append tname (Long_Name.base_name cname));
val atomT = Type (atom, []);
fun process_constr ((dts, dt), (j, args1, args2)) =
@@ -1101,7 +1101,7 @@
(fn _ => indtac dt_induct indnames 1 THEN
ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
(abs_supp @ supp_atm @
- PureThy.get_thms thy8 ("fs_" ^ NameSpace.base_name atom ^ "1") @
+ PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
List.concat supp_thms))))),
length new_type_names))
end) atoms;
@@ -1233,9 +1233,9 @@
val fin_set_fresh = map (fn s =>
at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms;
val pt1_atoms = map (fn Type (s, _) =>
- PureThy.get_thm thy9 ("pt_" ^ NameSpace.base_name s ^ "1")) dt_atomTs;
+ PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs;
val pt2_atoms = map (fn Type (s, _) =>
- PureThy.get_thm thy9 ("pt_" ^ NameSpace.base_name s ^ "2") RS sym) dt_atomTs;
+ PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs;
val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'";
val fs_atoms = PureThy.get_thms thy9 "fin_supp";
val abs_supp = PureThy.get_thms thy9 "abs_supp";
@@ -1514,7 +1514,7 @@
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
(map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
- PureThy.hide_fact true (NameSpace.append (Sign.full_bname thy10 big_rec_name) "induct");
+ PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct");
(** equivariance **)
@@ -1560,7 +1560,7 @@
val rec_fin_supp_thms = map (fn aT =>
let
- val name = NameSpace.base_name (fst (dest_Type aT));
+ val name = Long_Name.base_name (fst (dest_Type aT));
val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
val aset = HOLogic.mk_setT aT;
val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
@@ -1599,7 +1599,7 @@
val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
let
- val name = NameSpace.base_name (fst (dest_Type aT));
+ val name = Long_Name.base_name (fst (dest_Type aT));
val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
val a = Free ("a", aT);
val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
@@ -2013,10 +2013,10 @@
val (reccomb_defs, thy12) =
thy11
|> Sign.add_consts_i (map (fn ((name, T), T') =>
- (Binding.name (NameSpace.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
+ (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
- (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
+ (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
set $ Free ("x", T) $ Free ("y", T'))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
--- a/src/HOL/Nominal/nominal_permeq.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Mon Mar 09 10:10:34 2009 +0100
@@ -110,7 +110,7 @@
Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
(if (applicable_app f) then
let
- val name = NameSpace.base_name n
+ val name = Long_Name.base_name n
val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst")
val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst")
in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
@@ -198,8 +198,8 @@
Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $
pi2 $ t)) =>
let
- val tname' = NameSpace.base_name tname
- val uname' = NameSpace.base_name uname
+ val tname' = Long_Name.base_name tname
+ val uname' = Long_Name.base_name uname
in
if pi1 <> pi2 then (* only apply the composition rule in this case *)
if T = U then
--- a/src/HOL/Nominal/nominal_primrec.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Mon Mar 09 10:10:34 2009 +0100
@@ -207,7 +207,7 @@
val frees = ls @ x :: rs;
val raw_rhs = list_abs_free (frees,
list_comb (Const (rec_name, dummyT), fs @ [Free x]))
- val def_name = Thm.def_name (NameSpace.base_name fname);
+ val def_name = Thm.def_name (Long_Name.base_name fname);
val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
val SOME var = get_first (fn ((b, _), mx) =>
if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
@@ -286,7 +286,7 @@
fold_map (apfst (snd o snd) oo
LocalTheory.define Thm.definitionK o fst) defs';
val qualify = Binding.qualify false
- (space_implode "_" (map (NameSpace.base_name o #1) defs));
+ (space_implode "_" (map (Long_Name.base_name o #1) defs));
val names_atts' = map (apfst qualify) names_atts;
val cert = cterm_of (ProofContext.theory_of lthy');
--- a/src/HOL/Nominal/nominal_thmdecls.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Mon Mar 09 10:10:34 2009 +0100
@@ -115,7 +115,7 @@
(Var (n,ty))) =>
let
(* FIXME: this should be an operation the library *)
- val class_name = (NameSpace.map_base_name (fn s => "pt_"^s) tyatm)
+ val class_name = (Long_Name.map_base_name (fn s => "pt_"^s) tyatm)
in
if (Sign.of_sort thy (ty,[class_name]))
then [(pi,typi)]
--- a/src/HOL/SetInterval.thy Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/SetInterval.thy Mon Mar 09 10:10:34 2009 +0100
@@ -59,13 +59,13 @@
"@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10)
"@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3INT _<_./ _)" 10)
-syntax (input)
+syntax (xsymbols)
"@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" 10)
"@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\<Union> _<_./ _)" 10)
"@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" 10)
"@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _<_./ _)" 10)
-syntax (xsymbols)
+syntax (latex output)
"@UNION_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" 10)
"@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00_ < _)/ _)" 10)
"@INTER_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00_ \<le> _)/ _)" 10)
--- a/src/HOL/Statespace/state_fun.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Statespace/state_fun.ML Mon Mar 09 10:10:34 2009 +0100
@@ -336,17 +336,17 @@
[] => ""
| c::cs => String.implode (Char.toUpper c::cs ))
-fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (NameSpace.base_name T)
- | mkName (TFree (x,_)) = mkUpper (NameSpace.base_name x)
- | mkName (TVar ((x,_),_)) = mkUpper (NameSpace.base_name x);
+fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (Long_Name.base_name T)
+ | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
+ | mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
fun is_datatype thy n = is_some (Symtab.lookup (DatatypePackage.get_datatypes thy) n);
fun mk_map "List.list" = Syntax.const "List.map"
- | mk_map n = Syntax.const ("StateFun.map_" ^ NameSpace.base_name n);
+ | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);
fun gen_constr_destr comp prfx thy (Type (T,[])) =
- Syntax.const (deco prfx (mkUpper (NameSpace.base_name T)))
+ Syntax.const (deco prfx (mkUpper (Long_Name.base_name T)))
| gen_constr_destr comp prfx thy (T as Type ("fun",_)) =
let val (argTs,rangeT) = strip_type T;
in comp
@@ -360,11 +360,11 @@
then (* datatype args are recursively embedded into val *)
(case argTs of
[argT] => comp
- ((Syntax.const (deco prfx (mkUpper (NameSpace.base_name T)))))
+ ((Syntax.const (deco prfx (mkUpper (Long_Name.base_name T)))))
((mk_map T $ gen_constr_destr comp prfx thy argT))
| _ => raise (TYPE ("StateFun.gen_constr_destr",[T'],[])))
else (* type args are not recursively embedded into val *)
- Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (NameSpace.base_name T)))
+ Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (Long_Name.base_name T)))
| gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr",[T],[]));
val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ a $ b) ""
--- a/src/HOL/Statespace/state_space.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML Mon Mar 09 10:10:34 2009 +0100
@@ -645,7 +645,7 @@
fun update_tr ctxt [s,Free (n,_),v] = gen_update_tr false ctxt n v s;
fun update_tr' ctxt [_$Free (prj,_),_$Free (inj,_),n as (_$Free (name,_)),(Const (k,_)$v),s] =
- if NameSpace.base_name k = NameSpace.base_name KN then
+ if Long_Name.base_name k = Long_Name.base_name KN then
(case get_comp (Context.Proof ctxt) name of
SOME (T,_) => if inj=inject_name T andalso prj=project_name T then
Syntax.const "_statespace_update" $ s $ n $ v
--- a/src/HOL/Tools/TFL/post.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/TFL/post.ML Mon Mar 09 10:10:34 2009 +0100
@@ -223,7 +223,7 @@
*---------------------------------------------------------------------------*)
fun define_i strict thy cs ss congs wfs fid R eqs =
let val {functional,pats} = Prim.mk_functional thy eqs
- val (thy, def) = Prim.wfrec_definition0 thy (NameSpace.base_name fid) R functional
+ val (thy, def) = Prim.wfrec_definition0 thy (Long_Name.base_name fid) R functional
val {induct, rules, tcs} =
simplify_defn strict thy cs ss congs wfs fid pats def
val rules' =
@@ -248,7 +248,7 @@
fun defer_i thy congs fid eqs =
let val {rules,R,theory,full_pats_TCs,SV,...} =
- Prim.lazyR_def thy (NameSpace.base_name fid) congs eqs
+ Prim.lazyR_def thy (Long_Name.base_name fid) congs eqs
val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
val dummy = writeln "Proving induction theorem ...";
val induction = Prim.mk_induction theory
--- a/src/HOL/Tools/TFL/tfl.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML Mon Mar 09 10:10:34 2009 +0100
@@ -349,7 +349,7 @@
| L => mk_functional_err
("The following clauses are redundant (covered by preceding clauses): " ^
commas (map (fn i => Int.toString (i + 1)) L))
- in {functional = Abs(NameSpace.base_name fname, ftype,
+ in {functional = Abs(Long_Name.base_name fname, ftype,
abstract_over (atom,
absfree(aname,atype, case_tm))),
pats = patts2}
--- a/src/HOL/Tools/datatype_abs_proofs.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Mon Mar 09 10:10:34 2009 +0100
@@ -235,10 +235,10 @@
val (reccomb_defs, thy2) =
thy1
|> Sign.add_consts_i (map (fn ((name, T), T') =>
- (Binding.name (NameSpace.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
+ (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
- (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
+ (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
set $ Free ("x", T) $ Free ("y", T'))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
@@ -316,8 +316,8 @@
val fns = (List.concat (Library.take (i, case_dummy_fns))) @
fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
- val decl = ((Binding.name (NameSpace.base_name name), caseT), NoSyn);
- val def = (Binding.name (NameSpace.base_name name ^ "_def"),
+ val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
+ val def = (Binding.name (Long_Name.base_name name ^ "_def"),
Logic.mk_equals (list_comb (Const (name, caseT), fns1),
list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
--- a/src/HOL/Tools/datatype_aux.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/datatype_aux.ML Mon Mar 09 10:10:34 2009 +0100
@@ -224,7 +224,7 @@
| mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]);
fun name_of_typ (Type (s, Ts)) =
- let val s' = NameSpace.base_name s
+ let val s' = Long_Name.base_name s
in space_implode "_" (List.filter (not o equal "") (map name_of_typ Ts) @
[if Syntax.is_identifier s' then s' else "x"])
end
--- a/src/HOL/Tools/datatype_package.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML Mon Mar 09 10:10:34 2009 +0100
@@ -174,9 +174,9 @@
fun dt_cases (descr: descr) (_, args, constrs) =
let
- fun the_bname i = NameSpace.base_name (#1 (the (AList.lookup (op =) descr i)));
+ fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
val bnames = map the_bname (distinct (op =) (maps dt_recs args));
- in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end;
+ in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
fun induct_cases descr =
@@ -519,7 +519,7 @@
val cs = map (apsnd (map norm_constr)) raw_cs;
val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
o fst o strip_type;
- val new_type_names = map NameSpace.base_name (the_default (map fst cs) alt_names);
+ val new_type_names = map Long_Name.base_name (the_default (map fst cs) alt_names);
fun mk_spec (i, (tyco, constr)) = (i, (tyco,
map (DtTFree o fst) vs,
--- a/src/HOL/Tools/datatype_prop.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/datatype_prop.ML Mon Mar 09 10:10:34 2009 +0100
@@ -47,7 +47,7 @@
let
fun type_name (TFree (name, _)) = implode (tl (explode name))
| type_name (Type (name, _)) =
- let val name' = NameSpace.base_name name
+ let val name' = Long_Name.base_name name
in if Syntax.is_identifier name' then name' else "x" end;
in indexify_names (map type_name Ts) end;
--- a/src/HOL/Tools/datatype_realizer.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Mon Mar 09 10:10:34 2009 +0100
@@ -168,7 +168,7 @@
val Ts = map (typ_of_dtyp descr sorts) cargs;
val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts;
val free_ts = map Free frees;
- val r = Free ("r" ^ NameSpace.base_name cname, Ts ---> rT)
+ val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
(HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
--- a/src/HOL/Tools/datatype_rep_proofs.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Mon Mar 09 10:10:34 2009 +0100
@@ -236,7 +236,7 @@
val lhs = list_comb (Const (cname, constrT), l_args);
val rhs = mk_univ_inj r_args n i;
val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs);
- val def_name = NameSpace.base_name cname ^ "_def";
+ val def_name = Long_Name.base_name cname ^ "_def";
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
(Const (rep_name, T --> Univ_elT) $ lhs, rhs));
val ([def_thm], thy') =
@@ -343,7 +343,7 @@
val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
val fTs = map fastype_of fs;
- val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (NameSpace.base_name iso_name ^ "_def"),
+ val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Long_Name.base_name iso_name ^ "_def"),
Logic.mk_equals (Const (iso_name, T --> Univ_elT),
list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
val (def_thms, thy') =
--- a/src/HOL/Tools/function_package/fundef_package.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Mon Mar 09 10:10:34 2009 +0100
@@ -54,7 +54,7 @@
val simps_by_f = sort saved_simps
fun add_for_f fname simps =
- note_theorem ((NameSpace.qualified fname label, []), simps) #> snd
+ note_theorem ((Long_Name.qualify fname label, []), simps) #> snd
in
(saved_simps,
fold2 add_for_f fnames simps_by_f lthy)
@@ -66,12 +66,12 @@
cont (Thm.close_derivation proof)
val fnames = map (fst o fst) fixes
- val qualify = NameSpace.qualified defname
+ val qualify = Long_Name.qualify defname
val addsmps = add_simps fnames post sort_cont
val (((psimps', pinducts'), (_, [termination'])), lthy) =
lthy
- |> addsmps (NameSpace.qualified "partial") "psimps"
+ |> addsmps (Long_Name.qualify "partial") "psimps"
[Attrib.internal (K Nitpick_Const_Psimp_Thms.add)] psimps
||> fold_option (snd oo addsmps I "simps" [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]) trsimps
||>> note_theorem ((qualify "pinduct",
@@ -131,7 +131,7 @@
val allatts = (not has_guards ? cons Code.add_default_eqn_attrib)
[Attrib.internal (K Nitpick_Const_Simp_Thms.add)]
- val qualify = NameSpace.qualified defname;
+ val qualify = Long_Name.qualify defname;
in
lthy
|> add_simps I "simps" allatts tsimps |> snd
--- a/src/HOL/Tools/function_package/size.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML Mon Mar 09 10:10:34 2009 +0100
@@ -87,7 +87,7 @@
recTs1 ~~ alt_names' |>
map (fn (T as Type (s, _), optname) =>
let
- val s' = the_default (NameSpace.base_name s) optname ^ "_size";
+ val s' = the_default (Long_Name.base_name s) optname ^ "_size";
val s'' = Sign.full_bname thy s'
in
(s'',
@@ -140,7 +140,7 @@
val ((size_def_thms, size_def_thms'), thy') =
thy
|> Sign.add_consts_i (map (fn (s, T) =>
- (Binding.name (NameSpace.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
+ (Binding.name (Long_Name.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
(size_names ~~ recTs1))
|> PureThy.add_defs false
(map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
@@ -221,8 +221,8 @@
fun add_size_thms (new_type_names as name :: _) thy =
let
val info as {descr, alt_names, ...} = DatatypePackage.the_datatype thy name;
- val prefix = NameSpace.map_base_name (K (space_implode "_"
- (the_default (map NameSpace.base_name new_type_names) alt_names))) name;
+ val prefix = Long_Name.map_base_name (K (space_implode "_"
+ (the_default (map Long_Name.base_name new_type_names) alt_names))) name;
val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) descr
in if no_size then thy
--- a/src/HOL/Tools/inductive_package.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Mon Mar 09 10:10:34 2009 +0100
@@ -698,7 +698,7 @@
ctxt1 |>
LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>>
fold_map (fn (name, (elim, cases)) =>
- LocalTheory.note kind ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "cases"),
+ LocalTheory.note kind ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "cases"),
[Attrib.internal (K (RuleCases.case_names cases)),
Attrib.internal (K (RuleCases.consumes 1)),
Attrib.internal (K (Induct.cases_pred name)),
--- a/src/HOL/Tools/inductive_realizer.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Mon Mar 09 10:10:34 2009 +0100
@@ -68,8 +68,8 @@
val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
(Logic.strip_imp_concl (prop_of (hd intrs))));
val params = map dest_Var (Library.take (nparms, ts));
- val tname = Binding.name (space_implode "_" (NameSpace.base_name s ^ "T" :: vs));
- fun constr_of_intr intr = (Binding.name (NameSpace.base_name (name_of_thm intr)),
+ val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
+ fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
filter_out (equal Extraction.nullT) (map
(Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
@@ -112,7 +112,7 @@
val rT = if n then Extraction.nullT
else Type (space_implode "_" (s ^ "T" :: vs),
map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
- val r = if n then Extraction.nullt else Var ((NameSpace.base_name s, 0), rT);
+ val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
val S = list_comb (h, params @ xs);
val rvs = relevant_vars S;
val vs' = map fst rvs \\ vs;
@@ -195,7 +195,7 @@
in if conclT = Extraction.nullT
then list_abs_free (map dest_Free xs, HOLogic.unit)
else list_abs_free (map dest_Free xs, list_comb
- (Free ("r" ^ NameSpace.base_name (name_of_thm intr),
+ (Free ("r" ^ Long_Name.base_name (name_of_thm intr),
map fastype_of (rev args) ---> conclT), rev args))
end
@@ -217,7 +217,7 @@
end) (premss ~~ dummies);
val frees = fold Term.add_frees fs [];
val Ts = map fastype_of fs;
- fun name_of_fn intr = "r" ^ NameSpace.base_name (name_of_thm intr)
+ fun name_of_fn intr = "r" ^ Long_Name.base_name (name_of_thm intr)
in
fst (fold_map (fn concl => fn names =>
let val T = Extraction.etype_of thy vs [] concl
@@ -245,7 +245,7 @@
|-> (fn dtinfo => pair (map fst dts, SOME dtinfo))
handle DatatypeAux.Datatype_Empty name' =>
let
- val name = NameSpace.base_name name';
+ val name = Long_Name.base_name name';
val dname = Name.variant used "Dummy";
in
thy
@@ -273,8 +273,8 @@
fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
let
- val qualifier = NameSpace.qualifier (name_of_thm induct);
- val inducts = PureThy.get_thms thy (NameSpace.qualified qualifier "inducts");
+ val qualifier = Long_Name.qualifier (name_of_thm induct);
+ val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts");
val iTs = OldTerm.term_tvars (prop_of (hd intrs));
val ar = length vs + length iTs;
val params = InductivePackage.params_of raw_induct;
@@ -285,18 +285,18 @@
val rss' = map (fn (((s, rs), (_, arity)), elim) =>
(s, (InductivePackage.infer_intro_vars elim arity rs ~~ rs)))
(rss ~~ arities ~~ elims);
- val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
+ val (prfx, _) = split_last (Long_Name.explode (fst (hd rss)));
val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
val thy1 = thy |>
Sign.root_path |>
- Sign.add_path (NameSpace.implode prfx);
+ Sign.add_path (Long_Name.implode prfx);
val (ty_eqs, rlz_eqs) = split_list
(map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss);
val thy1' = thy1 |>
Theory.copy |>
- Sign.add_types (map (fn s => (Binding.name (NameSpace.base_name s), ar, NoSyn)) tnames) |>
+ Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
fold (fn s => AxClass.axiomatize_arity
(s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
Extraction.add_typeof_eqns_i ty_eqs;
@@ -334,7 +334,7 @@
rintrs |> map (fn rintr =>
let
val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr));
- val s' = NameSpace.base_name s;
+ val s' = Long_Name.base_name s;
val T' = Logic.unvarifyT T;
in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end)
|> distinct (op = o pairself (#1 o #1))
@@ -352,7 +352,7 @@
{quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
rlzpreds rlzparams (map (fn (rintr, intr) =>
- ((Binding.name (NameSpace.base_name (name_of_thm intr)), []),
+ ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
subst_atomic rlzpreds' (Logic.unvarify rintr)))
(rintrs ~~ maps snd rss)) [] ||>
Sign.absolute_path;
@@ -395,12 +395,12 @@
[K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
- (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
+ (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
(DatatypeAux.split_conj_thm thm');
val ([thms'], thy'') = PureThy.add_thmss
[((Binding.name (space_implode "_"
- (NameSpace.qualified qualifier "inducts" :: vs' @ Ps @
+ (Long_Name.qualify qualifier "inducts" :: vs' @ Ps @
["correctness"])), thms), [])] thy';
val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
in
@@ -409,7 +409,7 @@
mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
realizers @ (case realizers of
[(((ind, corr), rlz), r)] =>
- [mk_realizer thy' (vs' @ Ps) (NameSpace.qualified qualifier "induct",
+ [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
ind, corr, rlz, r)]
| _ => [])) thy''
end;
--- a/src/HOL/Tools/metis_tools.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML Mon Mar 09 10:10:34 2009 +0100
@@ -608,7 +608,7 @@
val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
in
if null unused then ()
- else warning ("Unused theorems: " ^ commas (map #1 unused));
+ else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
case result of
(_,ith)::_ =>
(Output.debug (fn () => "success: " ^ Display.string_of_thm ith);
--- a/src/HOL/Tools/old_primrec_package.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML Mon Mar 09 10:10:34 2009 +0100
@@ -212,7 +212,7 @@
((map snd ls) @ [dummyT])
(list_comb (Const (rec_name, dummyT),
fs @ map Bound (0 ::(length ls downto 1))))
- val def_name = NameSpace.base_name fname ^ "_" ^ NameSpace.base_name tname ^ "_def";
+ val def_name = Long_Name.base_name fname ^ "_" ^ Long_Name.base_name tname ^ "_def";
val def_prop =
singleton (Syntax.check_terms (ProofContext.init thy))
(Logic.mk_equals (Const (fname, dummyT), rhs));
@@ -269,7 +269,7 @@
else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
"\nare not mutually recursive");
val primrec_name =
- if alt_name = "" then (space_implode "_" (map (NameSpace.base_name o #1) defs)) else alt_name;
+ if alt_name = "" then (space_implode "_" (map (Long_Name.base_name o #1) defs)) else alt_name;
val (defs_thms', thy') =
thy
|> Sign.add_path primrec_name
--- a/src/HOL/Tools/primrec_package.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML Mon Mar 09 10:10:34 2009 +0100
@@ -191,7 +191,7 @@
(map snd ls @ [dummyT])
(list_comb (Const (rec_name, dummyT),
fs @ map Bound (0 :: (length ls downto 1))))
- val def_name = Thm.def_name (NameSpace.base_name fname);
+ val def_name = Thm.def_name (Long_Name.base_name fname);
val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
val SOME var = get_first (fn ((b, _), mx) =>
if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
@@ -247,7 +247,7 @@
val _ = if gen_eq_set (op =) (names1, names2) then ()
else primrec_error ("functions " ^ commas_quote names2 ^
"\nare not mutually recursive");
- val prefix = space_implode "_" (map (NameSpace.base_name o #1) defs);
+ val prefix = space_implode "_" (map (Long_Name.base_name o #1) defs);
val qualify = Binding.qualify false prefix;
val spec' = (map o apfst)
(fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
--- a/src/HOL/Tools/recdef_package.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML Mon Mar 09 10:10:34 2009 +0100
@@ -193,7 +193,7 @@
val _ = requires_recdef thy;
val name = Sign.intern_const thy raw_name;
- val bname = NameSpace.base_name name;
+ val bname = Long_Name.base_name name;
val _ = writeln ("Defining recursive function " ^ quote name ^ " ...");
val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
@@ -233,7 +233,7 @@
fun gen_defer_recdef tfl_fn eval_thms raw_name eqs raw_congs thy =
let
val name = Sign.intern_const thy raw_name;
- val bname = NameSpace.base_name name;
+ val bname = Long_Name.base_name name;
val _ = requires_recdef thy;
val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");
--- a/src/HOL/Tools/record_package.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/record_package.ML Mon Mar 09 10:10:34 2009 +0100
@@ -122,7 +122,7 @@
(* syntax *)
fun prune n xs = Library.drop (n, xs);
-fun prefix_base s = NameSpace.map_base_name (fn bname => s ^ bname);
+fun prefix_base s = Long_Name.map_base_name (fn bname => s ^ bname);
val Trueprop = HOLogic.mk_Trueprop;
fun All xs t = Term.list_all_free (xs, t);
@@ -433,8 +433,8 @@
fun get_extT_fields thy T =
let
val ((name,Ts),moreT) = dest_recT T;
- val recname = let val (nm::recn::rst) = rev (NameSpace.explode name)
- in NameSpace.implode (rev (nm::rst)) end;
+ val recname = let val (nm::recn::rst) = rev (Long_Name.explode name)
+ in Long_Name.implode (rev (nm::rst)) end;
val midx = maxidx_of_typs (moreT::Ts);
val varifyT = varifyT midx;
val {records,extfields,...} = RecordsData.get thy;
@@ -702,7 +702,7 @@
SOME flds
=> (let
val (f::fs) = but_last (map fst flds);
- val flds' = Sign.extern_const thy f :: map NameSpace.base_name fs;
+ val flds' = Sign.extern_const thy f :: map Long_Name.base_name fs;
val (args',more) = split_last args;
in (flds'~~args')@field_lst more end
handle Library.UnequalLengths => [("",t)])
@@ -804,7 +804,7 @@
=> (let
val (f :: fs) = but_last flds;
val flds' = apfst (Sign.extern_const thy) f
- :: map (apfst NameSpace.base_name) fs;
+ :: map (apfst Long_Name.base_name) fs;
val (args', more) = split_last args;
val alphavars = map varifyT (but_last alphas);
val subst = fold2 (curry (Sign.typ_match thy))
@@ -1069,7 +1069,7 @@
val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get thy;
(*fun mk_abs_var x t = (x, fastype_of t);*)
- fun sel_name u = NameSpace.base_name (unsuffix updateN u);
+ fun sel_name u = Long_Name.base_name (unsuffix updateN u);
fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
if has_field extfields s (domain_type' mT) then upd else seed s r
@@ -1461,7 +1461,7 @@
Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = TypedefPackage.get_info thy name;
val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp];
in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end;
- val tname = Binding.name (NameSpace.base_name name);
+ val tname = Binding.name (Long_Name.base_name name);
in
thy
|> TypecopyPackage.add_typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE
@@ -1475,7 +1475,7 @@
fun extension_definition full name fields names alphas zeta moreT more vars thy =
let
- val base = NameSpace.base_name;
+ val base = Long_Name.base_name;
val fieldTs = (map snd fields);
val alphas_zeta = alphas@[zeta];
val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
@@ -1761,7 +1761,7 @@
val alphas = map fst args;
val name = Sign.full_bname thy bname;
val full = Sign.full_bname_path thy bname;
- val base = NameSpace.base_name;
+ val base = Long_Name.base_name;
val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
@@ -1887,11 +1887,11 @@
fun parent_more s =
if null parents then s
- else mk_sel s (NameSpace.qualified (#name (List.last parents)) moreN, extT);
+ else mk_sel s (Long_Name.qualify (#name (List.last parents)) moreN, extT);
fun parent_more_upd v s =
if null parents then v$s
- else let val mp = NameSpace.qualified (#name (List.last parents)) moreN;
+ else let val mp = Long_Name.qualify (#name (List.last parents)) moreN;
in mk_upd updateN mp v s end;
(*record (scheme) type abbreviation*)
--- a/src/HOL/Tools/res_atp.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/res_atp.ML Mon Mar 09 10:10:34 2009 +0100
@@ -303,7 +303,7 @@
(*Reject theorems with names like "List.filter.filter_list_def" or
"Accessible_Part.acc.defs", as these are definitions arising from packages.*)
fun is_package_def a =
- let val names = NameSpace.explode a
+ let val names = Long_Name.explode a
in
length names > 2 andalso
not (hd names = "local") andalso
@@ -378,7 +378,7 @@
(*Ignore blacklisted basenames*)
fun add_multi_names ((a, ths), pairs) =
- if (NameSpace.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs
+ if (Long_Name.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs
else add_single_names ((a, ths), pairs);
fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
--- a/src/HOL/Tools/res_axioms.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Mon Mar 09 10:10:34 2009 +0100
@@ -328,7 +328,7 @@
"cases","ext_cases"]; (*FIXME: put other record thms here, or use the "Internal" marker*)
(*Keep the full complexity of the original name*)
-fun flatten_name s = space_implode "_X" (NameSpace.explode s);
+fun flatten_name s = space_implode "_X" (Long_Name.explode s);
fun fake_name th =
if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
@@ -340,7 +340,7 @@
(*Skolemize a named theorem, with Skolem functions as additional premises.*)
fun skolem_thm (s, th) =
- if member (op =) multi_base_blacklist (NameSpace.base_name s) orelse bad_for_atp th then []
+ if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse bad_for_atp th then []
else
let
val ctxt0 = Variable.thm_context th
@@ -428,7 +428,7 @@
val new_facts = (PureThy.facts_of thy, []) |-> Facts.fold_static (fn (name, ths) =>
if already_seen thy name then I else cons (name, ths));
val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
- if member (op =) multi_base_blacklist (NameSpace.base_name name) then I
+ if member (op =) multi_base_blacklist (Long_Name.base_name name) then I
else fold_index (fn (i, th) =>
if bad_for_atp th orelse is_some (lookup_cache thy th) then I
else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths);
--- a/src/HOL/Tools/specification_package.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/Tools/specification_package.ML Mon Mar 09 10:10:34 2009 +0100
@@ -24,7 +24,7 @@
val ctype = domain_type (type_of P)
val cname_full = Sign.intern_const thy cname
val cdefname = if thname = ""
- then Thm.def_name (NameSpace.base_name cname)
+ then Thm.def_name (Long_Name.base_name cname)
else thname
val def_eq = Logic.mk_equals (Const(cname_full,ctype),
HOLogic.choice_const ctype $ P)
@@ -50,7 +50,7 @@
val ctype = domain_type (type_of P)
val cname_full = Sign.intern_const thy cname
val cdefname = if thname = ""
- then Thm.def_name (NameSpace.base_name cname)
+ then Thm.def_name (Long_Name.base_name cname)
else thname
val co = Const(cname_full,ctype)
val thy' = Theory.add_finals_i covld [co] thy
@@ -154,7 +154,7 @@
fun mk_exist (c,prop) =
let
val T = type_of c
- val cname = NameSpace.base_name (fst (dest_Const c))
+ val cname = Long_Name.base_name (fst (dest_Const c))
val vname = if Syntax.is_identifier cname
then cname
else "x"
--- a/src/HOL/ex/Quickcheck_Generators.thy Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOL/ex/Quickcheck_Generators.thy Mon Mar 09 10:10:34 2009 +0100
@@ -138,7 +138,7 @@
let
val this_ty = Type (hd tycos, map TFree vs);
val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed};
- val random_name = NameSpace.base_name @{const_name random};
+ val random_name = Long_Name.base_name @{const_name random};
val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'";
fun random ty = Sign.mk_const thy (@{const_name random}, [ty]);
val random' = Free (random'_name,
--- a/src/HOLCF/Tools/domain/domain_axioms.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML Mon Mar 09 10:10:34 2009 +0100
@@ -22,7 +22,7 @@
val dc_rep = %%:(dname^"_rep");
val x_name'= "x";
val x_name = idx_name eqs x_name' (n+1);
- val dnam = NameSpace.base_name dname;
+ val dnam = Long_Name.base_name dname;
val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
--- a/src/HOLCF/Tools/domain/domain_extender.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Mon Mar 09 10:10:34 2009 +0100
@@ -103,7 +103,7 @@
(Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
o fst) eqs''';
val cons''' = map snd eqs''';
- fun thy_type (dname,tvars) = (Binding.name (NameSpace.base_name dname), length tvars, NoSyn);
+ fun thy_type (dname,tvars) = (Binding.name (Long_Name.base_name dname), length tvars, NoSyn);
fun thy_arity (dname,tvars) = (dname, map (snd o dest_TFree) tvars, pcpoS);
val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
|> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
@@ -114,7 +114,7 @@
val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
fun typid (Type (id,_)) =
- let val c = hd (Symbol.explode (NameSpace.base_name id))
+ let val c = hd (Symbol.explode (Long_Name.base_name id))
in if Symbol.is_letter c then c else "t" end
| typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
| typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
@@ -133,7 +133,7 @@
||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
in
theorems_thy
- |> Sign.add_path (NameSpace.base_name comp_dnam)
+ |> Sign.add_path (Long_Name.base_name comp_dnam)
|> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])]))
|> Sign.parent_path
end;
--- a/src/HOLCF/Tools/domain/domain_syntax.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML Mon Mar 09 10:10:34 2009 +0100
@@ -25,7 +25,7 @@
in
val dtype = Type(dname,typevars);
val dtype2 = foldr1 mk_ssumT (map prod cons');
- val dnam = NameSpace.base_name dname;
+ val dnam = Long_Name.base_name dname;
val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn);
val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn);
val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Mon Mar 09 10:10:34 2009 +0100
@@ -606,7 +606,7 @@
in
thy
- |> Sign.add_path (NameSpace.base_name dname)
+ |> Sign.add_path (Long_Name.base_name dname)
|> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
("iso_rews" , iso_rews ),
("exhaust" , [exhaust] ),
--- a/src/HOLCF/Tools/fixrec_package.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML Mon Mar 09 10:10:34 2009 +0100
@@ -181,7 +181,7 @@
val fixpoint = mk_fix (lambda_ctuple lhss (mk_ctuple rhss));
fun one_def (l as Free(n,_)) r =
- let val b = NameSpace.base_name n
+ let val b = Long_Name.base_name n
in ((Binding.name (b^"_def"), []), r) end
| one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
fun defs [] _ = []
@@ -230,7 +230,7 @@
fun taken_names (t : term) : bstring list =
let
- fun taken (Const(a,_), bs) = insert (op =) (NameSpace.base_name a) bs
+ fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
| taken (Free(a,_) , bs) = insert (op =) a bs
| taken (f $ u , bs) = taken (f, taken (u, bs))
| taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs)
--- a/src/Pure/General/ROOT.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/General/ROOT.ML Mon Mar 09 10:10:34 2009 +0100
@@ -26,6 +26,7 @@
use "ord_list.ML";
use "balanced_tree.ML";
use "graph.ML";
+use "long_name.ML";
use "binding.ML";
use "name_space.ML";
use "lazy.ML";
--- a/src/Pure/General/binding.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/General/binding.ML Mon Mar 09 10:10:34 2009 +0100
@@ -22,6 +22,7 @@
val eq_name: binding * binding -> bool
val empty: binding
val is_empty: binding -> bool
+ val qualified_name: bstring -> binding
val qualify: bool -> string -> binding -> binding
val prefix_of: binding -> (string * bool) list
val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
@@ -51,7 +52,7 @@
fun str_of (Binding {prefix, qualifier, name, pos}) =
let
- val text = space_implode "." (map #1 qualifier @ [name]);
+ val text = Long_Name.implode (map #1 qualifier @ [name]);
val props = Position.properties_of pos;
in Markup.markup (Markup.properties props (Markup.binding name)) text end;
@@ -79,6 +80,11 @@
(* user qualifier *)
+fun qualified_name "" = empty
+ | qualified_name s =
+ let val (qualifier, name) = split_last (Long_Name.explode s)
+ in make_binding ([], map (rpair false) qualifier, name, Position.none) end;
+
fun qualify _ "" = I
| qualify strict qual = map_binding (fn (prefix, qualifier, name, pos) =>
(prefix, (qual, strict) :: qualifier, name, pos));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/long_name.ML Mon Mar 09 10:10:34 2009 +0100
@@ -0,0 +1,49 @@
+(* Title: Pure/General/long_name.ML
+ Author: Makarius
+
+Long names.
+*)
+
+signature LONG_NAME =
+sig
+ val separator: string
+ val is_qualified: string -> bool
+ val implode: string list -> string
+ val explode: string -> string list
+ val append: string -> string -> string
+ val qualify: string -> string -> string
+ val qualifier: string -> string
+ val base_name: string -> string
+ val map_base_name: (string -> string) -> string -> string
+end;
+
+structure Long_Name: LONG_NAME =
+struct
+
+val separator = ".";
+val is_qualified = exists_string (fn s => s = separator);
+
+val implode = space_implode separator;
+val explode = space_explode separator;
+
+fun append name1 "" = name1
+ | append "" name2 = name2
+ | append name1 name2 = name1 ^ separator ^ name2;
+
+fun qualify qual name =
+ if qual = "" orelse name = "" then name
+ else qual ^ separator ^ name;
+
+fun qualifier "" = ""
+ | qualifier name = implode (#1 (split_last (explode name)));
+
+fun base_name "" = ""
+ | base_name name = List.last (explode name);
+
+fun map_base_name _ "" = ""
+ | map_base_name f name =
+ let val names = explode name
+ in implode (nth_map (length names - 1) f names) end;
+
+end;
+
--- a/src/Pure/General/name_space.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/General/name_space.ML Mon Mar 09 10:10:34 2009 +0100
@@ -19,15 +19,6 @@
include BASIC_NAME_SPACE
val hidden: string -> string
val is_hidden: string -> bool
- val separator: string (*single char*)
- val is_qualified: string -> bool
- val implode: string list -> string
- val explode: string -> string list
- val append: string -> string -> string
- val qualified: string -> string -> string
- val base_name: string -> string
- val qualifier: string -> string
- val map_base_name: (string -> string) -> string -> string
type T
val empty: T
val intern: T -> xstring -> string
@@ -64,32 +55,6 @@
fun hidden name = "??." ^ name;
val is_hidden = String.isPrefix "??.";
-val separator = ".";
-val is_qualified = exists_string (fn s => s = separator);
-
-val implode_name = space_implode separator;
-val explode_name = space_explode separator;
-
-fun append name1 "" = name1
- | append "" name2 = name2
- | append name1 name2 = name1 ^ separator ^ name2;
-
-fun qualified path name =
- if path = "" orelse name = "" then name
- else path ^ separator ^ name;
-
-fun base_name "" = ""
- | base_name name = List.last (explode_name name);
-
-fun qualifier "" = ""
- | qualifier name = implode_name (#1 (split_last (explode_name name)));
-
-fun map_base_name _ "" = ""
- | map_base_name f name =
- let val names = explode_name name
- in implode_name (nth_map (length names - 1) f names) end;
-
-
(* standard accesses *)
infixr 6 @@;
@@ -161,7 +126,7 @@
| ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
in
if long_names then name
- else if short_names then base_name name
+ else if short_names then Long_Name.base_name name
else ext (get_accesses space name)
end;
@@ -196,7 +161,7 @@
(* hide *)
fun hide fully name space =
- if not (is_qualified name) then
+ if not (Long_Name.is_qualified name) then
error ("Attempt to hide global name " ^ quote name)
else if is_hidden name then
error ("Attempt to hide hidden name " ^ quote name)
@@ -204,7 +169,8 @@
let val names = valid_accesses space name in
space
|> add_name' name name
- |> fold (del_name name) (if fully then names else names inter_string [base_name name])
+ |> fold (del_name name)
+ (if fully then names else names inter_string [Long_Name.base_name name])
|> fold (del_name_extra name) (get_accesses space name)
end;
@@ -237,33 +203,34 @@
fun path_of (Naming (path, _)) = path;
fun accesses (Naming (_, (_, accs))) = accs;
-fun external_names naming = map implode_name o #2 o accesses naming o explode_name;
+fun external_names naming = map Long_Name.implode o #2 o accesses naming o Long_Name.explode;
(* manipulate namings *)
fun reject_qualified name =
- if is_qualified name then
+ if Long_Name.is_qualified name then
error ("Attempt to declare qualified name " ^ quote name)
else name;
val default_naming =
- Naming ("", (fn path => qualified path o reject_qualified, suffixes_prefixes));
+ Naming ("", (fn path => Long_Name.qualify path o reject_qualified, suffixes_prefixes));
fun add_path elems (Naming (path, policy)) =
- if elems = "//" then Naming ("", (qualified, #2 policy))
+ if elems = "//" then Naming ("", (Long_Name.qualify, #2 policy))
else if elems = "/" then Naming ("", policy)
- else if elems = ".." then Naming (qualifier path, policy)
- else Naming (append path elems, policy);
+ else if elems = ".." then Naming (Long_Name.qualifier path, policy)
+ else Naming (Long_Name.append path elems, policy);
fun no_base_names (Naming (path, (qualify, accs))) =
Naming (path, (qualify, pairself (filter_out (fn [_] => true | _ => false)) o accs));
-fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
+fun qualified_names (Naming (path, (_, accs))) = Naming (path, (Long_Name.qualify, accs));
fun sticky_prefix prfx (Naming (path, (qualify, _))) =
- Naming (append path prfx,
- (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
+ Naming (Long_Name.append path prfx,
+ (qualify,
+ suffixes_prefixes_split (length (Long_Name.explode path)) (length (Long_Name.explode prfx))));
val apply_prefix =
let
@@ -290,13 +257,13 @@
val (prfx, bname) = Binding.dest binding;
val naming' = apply_prefix prfx naming;
val name = full naming' bname;
- val names = explode_name name;
+ val names = Long_Name.explode name;
val _ = (null names orelse exists (fn s => s = "" orelse s = "??") names
orelse exists_string (fn s => s = "\"") name) andalso
error ("Bad name declaration " ^ quote (Binding.str_of binding));
- val (accs, accs') = pairself (map implode_name) (accesses naming' names);
+ val (accs, accs') = pairself (map Long_Name.implode) (accesses naming' names);
val space' = space |> fold (add_name name) accs |> put_accesses name accs';
in (name, space') end;
@@ -325,11 +292,6 @@
fun dest_table tab = map (apfst #1) (ext_table tab);
fun extern_table tab = map (apfst #2) (ext_table tab);
-
-(*final declarations of this structure!*)
-val implode = implode_name;
-val explode = explode_name;
-
end;
structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
--- a/src/Pure/IsaMakefile Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/IsaMakefile Mon Mar 09 10:10:34 2009 +0100
@@ -48,28 +48,28 @@
General/alist.ML General/balanced_tree.ML General/basics.ML \
General/binding.ML General/buffer.ML General/file.ML \
General/graph.ML General/heap.ML General/integer.ML General/lazy.ML \
- General/markup.ML General/name_space.ML General/ord_list.ML \
- General/output.ML General/path.ML General/position.ML \
- General/pretty.ML General/print_mode.ML General/properties.ML \
- General/queue.ML General/scan.ML General/secure.ML General/seq.ML \
- General/source.ML General/stack.ML General/symbol.ML \
- General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML \
- General/yxml.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML \
- Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \
- Isar/class_target.ML Isar/code.ML Isar/code_unit.ML \
- Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
- Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \
- Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \
- Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML \
- Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
- Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
- Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
- Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
- Isar/rule_insts.ML Isar/skip_proof.ML Isar/spec_parse.ML \
- Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \
- Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_context.ML ML/ml_lex.ML \
- ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \
- ML-Systems/install_pp_polyml.ML Proof/extraction.ML \
+ General/long_name.ML General/markup.ML General/name_space.ML \
+ General/ord_list.ML General/output.ML General/path.ML \
+ General/position.ML General/pretty.ML General/print_mode.ML \
+ General/properties.ML General/queue.ML General/scan.ML \
+ General/secure.ML General/seq.ML General/source.ML General/stack.ML \
+ General/symbol.ML General/symbol_pos.ML General/table.ML \
+ General/url.ML General/xml.ML General/yxml.ML Isar/ROOT.ML \
+ Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
+ Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \
+ Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML \
+ Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML \
+ Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML \
+ Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \
+ Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \
+ Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \
+ Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \
+ Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
+ Isar/rule_cases.ML Isar/rule_insts.ML Isar/skip_proof.ML \
+ Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \
+ Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \
+ ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
+ ML/ml_thms.ML ML-Systems/install_pp_polyml.ML Proof/extraction.ML \
Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML \
ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \
--- a/src/Pure/Isar/class_target.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Isar/class_target.ML Mon Mar 09 10:10:34 2009 +0100
@@ -300,7 +300,7 @@
map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy;
fun redeclare_const thy c =
- let val b = NameSpace.base_name c
+ let val b = Long_Name.base_name c
in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
fun synchronize_class_syntax sort base_sort ctxt =
@@ -358,7 +358,7 @@
(* class target *)
-val class_prefix = Logic.const_of_class o NameSpace.base_name;
+val class_prefix = Logic.const_of_class o Long_Name.base_name;
fun declare class pos ((c, mx), dict) thy =
let
@@ -475,7 +475,7 @@
fun type_name "*" = "prod"
| type_name "+" = "sum"
- | type_name s = sanatize_name (NameSpace.base_name s);
+ | type_name s = sanatize_name (Long_Name.base_name s);
fun resort_terms pp algebra consts constraints ts =
let
--- a/src/Pure/Isar/element.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Isar/element.ML Mon Mar 09 10:10:34 2009 +0100
@@ -202,7 +202,7 @@
let val head =
if Thm.has_name_hint th then
Pretty.block [Pretty.command kind,
- Pretty.brk 1, Pretty.str (NameSpace.base_name (Thm.get_name_hint th) ^ ":")]
+ Pretty.brk 1, Pretty.str (Long_Name.base_name (Thm.get_name_hint th) ^ ":")]
else Pretty.command kind
in Pretty.block (Pretty.fbreaks (head :: prts)) end;
@@ -522,7 +522,7 @@
in (elems |> map (map_ctxt_attrib Args.closure), ProofContext.restore_naming ctxt ctxt') end;
fun check_name name =
- if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
+ if Long_Name.is_qualified name then error ("Illegal qualified name: " ^ quote name)
else name;
fun prep_facts prep_name get intern ctxt =
--- a/src/Pure/Isar/isar_cmd.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Mon Mar 09 10:10:34 2009 +0100
@@ -503,15 +503,15 @@
(* markup commands *)
-fun check_text (txt, pos) opt_node =
+fun check_text (txt, pos) state =
(Position.report Markup.doc_source pos;
- ignore (ThyOutput.eval_antiquote (#1 (OuterKeyword.get_lexicons ())) opt_node (txt, pos)));
+ ignore (ThyOutput.eval_antiquote (#1 (OuterKeyword.get_lexicons ())) state (txt, pos)));
fun header_markup txt = Toplevel.keep (fn state =>
- if Toplevel.is_toplevel state then check_text txt NONE
+ if Toplevel.is_toplevel state then check_text txt state
else raise Toplevel.UNDEF);
-fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (check_text txt o SOME);
-fun proof_markup txt = Toplevel.present_proof (check_text txt o SOME);
+fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (check_text txt);
+val proof_markup = Toplevel.present_proof o check_text;
end;
--- a/src/Pure/Isar/proof_context.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Mar 09 10:10:34 2009 +0100
@@ -590,7 +590,7 @@
let
val _ = no_skolem false x;
val sko = lookup_skolem ctxt x;
- val is_const = can (read_const_proper ctxt) x orelse NameSpace.is_qualified x;
+ val is_const = can (read_const_proper ctxt) x orelse Long_Name.is_qualified x;
val is_declared = is_some (def_type (x, ~1));
in
if Variable.is_const ctxt x then NONE
--- a/src/Pure/Isar/proof_display.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML Mon Mar 09 10:10:34 2009 +0100
@@ -75,7 +75,7 @@
fun pretty_fact_name (kind, "") = Pretty.str kind
| pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
- Pretty.str (NameSpace.base_name name), Pretty.str ":"];
+ Pretty.str (Long_Name.base_name name), Pretty.str ":"];
fun pretty_facts ctxt =
flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
--- a/src/Pure/Isar/rule_cases.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Isar/rule_cases.ML Mon Mar 09 10:10:34 2009 +0100
@@ -105,7 +105,7 @@
if not nested then abs_fixes t
else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
- val (assumes1, assumes2) = extract_assumes (NameSpace.qualified name) case_outline prop
+ val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) case_outline prop
|> pairself (map (apsnd (maps Logic.dest_conjunctions)));
val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop);
--- a/src/Pure/Isar/theory_target.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML Mon Mar 09 10:10:34 2009 +0100
@@ -329,7 +329,7 @@
fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
Data.put ta #>
- LocalTheory.init (NameSpace.base_name target)
+ LocalTheory.init (Long_Name.base_name target)
{pretty = pretty ta,
abbrev = abbrev ta,
define = define ta,
--- a/src/Pure/Isar/toplevel.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Mar 09 10:10:34 2009 +0100
@@ -13,7 +13,6 @@
val proof_node: node -> ProofNode.T option
val cases_node: (generic_theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a
val context_node: node -> Proof.context
- val presentation_context: node option -> xstring option -> Proof.context
type state
val toplevel: state
val is_toplevel: state -> bool
@@ -23,6 +22,7 @@
val previous_node_of: state -> node option
val node_of: state -> node
val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
+ val presentation_context_of: state -> xstring option -> Proof.context
val context_of: state -> Proof.context
val generic_theory_of: state -> generic_theory
val theory_of: state -> theory
@@ -68,7 +68,7 @@
val local_theory': xstring option -> (bool -> local_theory -> local_theory) ->
transition -> transition
val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
- val present_local_theory: xstring option -> (node -> unit) -> transition -> transition
+ val present_local_theory: xstring option -> (state -> unit) -> transition -> transition
val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
transition -> transition
val local_theory_to_proof: xstring option -> (local_theory -> Proof.state) ->
@@ -76,7 +76,7 @@
val theory_to_proof: (theory -> Proof.state) -> transition -> transition
val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
val forget_proof: transition -> transition
- val present_proof: (node -> unit) -> transition -> transition
+ val present_proof: (state -> unit) -> transition -> transition
val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition
val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
@@ -145,15 +145,6 @@
val context_node = cases_node Context.proof_of Proof.context_of;
-fun presentation_context (SOME (Theory (_, SOME ctxt))) NONE = ctxt
- | presentation_context (SOME node) NONE = context_node node
- | presentation_context (SOME node) (SOME loc) =
- loc_init loc (cases_node Context.theory_of Proof.theory_of node)
- | presentation_context NONE _ = raise UNDEF;
-
-fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE)
- | reset_presentation node = node;
-
(* datatype state *)
@@ -189,6 +180,13 @@
fun node_case f g state = cases_node f g (node_of state);
+fun presentation_context_of state opt_loc =
+ (case (try node_of state, opt_loc) of
+ (SOME (Theory (_, SOME ctxt)), NONE) => ctxt
+ | (SOME node, NONE) => context_node node
+ | (SOME node, SOME loc) => loc_init loc (cases_node Context.theory_of Proof.theory_of node)
+ | (NONE, _) => raise UNDEF);
+
val context_of = node_case Context.proof_of Proof.context_of;
val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
val theory_of = node_case Context.theory_of Proof.theory_of;
@@ -324,6 +322,9 @@
local
+fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE)
+ | reset_presentation node = node;
+
fun is_draft_theory (Theory (gthy, _)) = Context.is_draft (Context.theory_of gthy)
| is_draft_theory _ = false;
@@ -338,7 +339,7 @@
in
-fun apply_transaction pos f (node, exit) =
+fun apply_transaction pos f g (node, exit) =
let
val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state";
val cont_node = reset_presentation node;
@@ -357,7 +358,7 @@
else (result, err);
in
(case err' of
- NONE => result'
+ NONE => tap g result'
| SOME exn => raise FAILURE (result', exn))
end;
@@ -371,7 +372,7 @@
Exit | (*formal exit of theory -- without committing*)
CommitExit | (*exit and commit final theory*)
Keep of bool -> state -> unit | (*peek at state*)
- Transaction of bool -> node -> node; (*node transaction*)
+ Transaction of (bool -> node -> node) * (state -> unit); (*node transaction and presentation*)
local
@@ -383,8 +384,8 @@
(controlled_execution exit thy; toplevel)
| apply_tr int _ (Keep f) state =
controlled_execution (fn x => tap (f int) x) state
- | apply_tr int pos (Transaction f) (State (SOME state, _)) =
- apply_transaction pos (fn x => f int x) state
+ | apply_tr int pos (Transaction (f, g)) (State (SOME state, _)) =
+ apply_transaction pos (fn x => f int x) g state
| apply_tr _ _ _ _ = raise UNDEF;
fun apply_union _ _ [] state = raise FAILURE (state, UNDEF)
@@ -470,7 +471,9 @@
fun init_theory name f exit = add_trans (Init (name, f, exit));
val exit = add_trans Exit;
val keep' = add_trans o Keep;
-fun transaction f = add_trans (Transaction f);
+
+fun present_transaction f g = add_trans (Transaction (f, g));
+fun transaction f = present_transaction f (K ());
fun keep f = add_trans (Keep (fn _ => f));
fun imperative f = keep (fn _ => f ());
@@ -510,19 +513,19 @@
local
-fun local_theory_presentation loc f g = transaction (fn int =>
+fun local_theory_presentation loc f = present_transaction (fn int =>
(fn Theory (gthy, _) =>
let
val finish = loc_finish loc gthy;
val lthy' = f int (loc_begin loc gthy);
in Theory (finish lthy', SOME lthy') end
- | _ => raise UNDEF) #> tap g);
+ | _ => raise UNDEF));
in
-fun local_theory' loc f = local_theory_presentation loc f (K I);
+fun local_theory' loc f = local_theory_presentation loc f (K ());
fun local_theory loc f = local_theory' loc (K f);
-fun present_local_theory loc g = local_theory_presentation loc (K I) g;
+fun present_local_theory loc = local_theory_presentation loc (K I);
end;
@@ -579,10 +582,10 @@
| SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
| _ => raise UNDEF));
-fun present_proof f = transaction (fn _ =>
+val present_proof = present_transaction (fn _ =>
(fn Proof (prf, x) => Proof (ProofNode.apply I prf, x)
| skip as SkipProof _ => skip
- | _ => raise UNDEF) #> tap f);
+ | _ => raise UNDEF));
fun proofs' f = transaction (fn int =>
(fn Proof (prf, x) => Proof (ProofNode.applys (f int) prf, x)
@@ -734,18 +737,18 @@
val future_proof = Proof.global_future_proof
(fn prf =>
Future.fork_pri ~1 (fn () =>
- let val (states, State (result_node, _)) =
+ let val (states, result_state) =
(case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
=> State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
|> fold_map command_result body_trs
||> command (end_tr |> set_print false);
- in (states, presentation_context (Option.map #1 result_node) NONE) end))
+ in (states, presentation_context_of result_state NONE) end))
#> (fn (states, ctxt) => States.put (SOME states) ctxt);
val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
val states =
- (case States.get (presentation_context (SOME (node_of st'')) NONE) of
+ (case States.get (presentation_context_of st'' NONE) of
NONE => sys_error ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
| SOME states => states);
val result = Lazy.lazy
--- a/src/Pure/ML/ml_antiquote.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Mon Mar 09 10:10:34 2009 +0100
@@ -110,7 +110,7 @@
fun type_ syn = (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
#1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
- |> syn ? NameSpace.base_name
+ |> syn ? Long_Name.base_name
|> ML_Syntax.print_string));
val _ = inline "type_name" (type_ false);
--- a/src/Pure/Proof/extraction.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Mon Mar 09 10:10:34 2009 +0100
@@ -119,7 +119,7 @@
val chtype = change_type o SOME;
-fun extr_name s vs = NameSpace.append "extr" (space_implode "_" (s :: vs));
+fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
fun corr_name s vs = extr_name s vs ^ "_correctness";
fun msg d s = priority (Symbol.spaces d ^ s);
--- a/src/Pure/Proof/proof_syntax.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Mon Mar 09 10:10:34 2009 +0100
@@ -97,16 +97,16 @@
fun prf_of [] (Bound i) = PBound i
| prf_of Ts (Const (s, Type ("proof", _))) =
change_type (if ty then SOME Ts else NONE)
- (case NameSpace.explode s of
+ (case Long_Name.explode s of
"axm" :: xs =>
let
- val name = NameSpace.implode xs;
+ val name = Long_Name.implode xs;
val prop = (case AList.lookup (op =) axms name of
SOME prop => prop
| NONE => error ("Unknown axiom " ^ quote name))
in PAxm (name, prop, NONE) end
| "thm" :: xs =>
- let val name = NameSpace.implode xs;
+ let val name = Long_Name.implode xs;
in (case AList.lookup (op =) thms name of
SOME thm => fst (strip_combt (Thm.proof_of thm))
| NONE => error ("Unknown theorem " ^ quote name))
@@ -147,12 +147,12 @@
[proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
fun term_of _ (PThm (_, ((name, _, NONE), _))) =
- Const (NameSpace.append "thm" name, proofT)
+ Const (Long_Name.append "thm" name, proofT)
| term_of _ (PThm (_, ((name, _, SOME Ts), _))) =
- mk_tyapp Ts (Const (NameSpace.append "thm" name, proofT))
- | term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT)
+ mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT))
+ | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT)
| term_of _ (PAxm (name, _, SOME Ts)) =
- mk_tyapp Ts (Const (NameSpace.append "axm" name, proofT))
+ mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT))
| term_of _ (PBound i) = Bound i
| term_of Ts (Abst (s, opT, prf)) =
let val T = the_default dummyT opT
@@ -183,7 +183,7 @@
val thy' = thy
|> add_proof_syntax
|> add_proof_atom_consts
- (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names);
+ (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names);
in
(cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
end;
@@ -195,7 +195,7 @@
val ctxt = thy
|> add_proof_syntax
|> add_proof_atom_consts
- (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names)
+ (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
|> ProofContext.init
|> ProofContext.allow_dummies
|> ProofContext.set_mode ProofContext.mode_schematic;
@@ -219,7 +219,7 @@
in
add_proof_syntax #>
add_proof_atom_consts
- (map (NameSpace.append "thm") thm_names @ map (NameSpace.append "axm") axm_names)
+ (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
end;
fun proof_of full thm =
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Mar 09 10:10:34 2009 +0100
@@ -543,8 +543,8 @@
fun setids t = issue_pgip (Setids {idtables = [t]})
(* fake one-level nested "subtheories" by picking apart names. *)
- val immed_thms_of_thy = filter_out NameSpace.is_qualified o thms_of_thy
- fun thy_prefix s = case space_explode NameSpace.separator s of
+ val immed_thms_of_thy = filter_out Long_Name.is_qualified o thms_of_thy
+ fun thy_prefix s = case Long_Name.explode s of
x::_::_ => SOME x (* String.find? *)
| _ => NONE
fun subthys_of_thy s =
@@ -553,7 +553,7 @@
fun subthms_of_thy thy =
(case thy_prefix thy of
NONE => immed_thms_of_thy thy
- | SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy))
+ | SOME prf => filter (String.isPrefix (unprefix (prf ^ Long_Name.separator) thy))
(thms_of_thy prf))
in
case (thyname,objtype) of
@@ -642,7 +642,7 @@
val topthy = Toplevel.theory_of o Isar.state
fun splitthy id =
- let val comps = NameSpace.explode id
+ let val comps = Long_Name.explode id
in case comps of
(thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
| [plainid] => (topthy(),plainid)
--- a/src/Pure/Syntax/syntax.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Syntax/syntax.ML Mon Mar 09 10:10:34 2009 +0100
@@ -301,7 +301,7 @@
lexicon =
if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
gram = if changed then Parser.extend_gram gram xprods else gram,
- consts = Library.merge (op =) (consts1, filter_out NameSpace.is_qualified consts2),
+ consts = Library.merge (op =) (consts1, filter_out Long_Name.is_qualified consts2),
prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
parse_ast_trtab =
update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
@@ -607,7 +607,7 @@
fun constify (ast as Ast.Constant _) = ast
| constify (ast as Ast.Variable x) =
- if member (op =) consts x orelse NameSpace.is_qualified x then Ast.Constant x
+ if member (op =) consts x orelse Long_Name.is_qualified x then Ast.Constant x
else ast
| constify (Ast.Appl asts) = Ast.Appl (map constify asts);
--- a/src/Pure/Syntax/type_ext.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Syntax/type_ext.ML Mon Mar 09 10:10:34 2009 +0100
@@ -129,7 +129,7 @@
(case (map_free a, map_const a) of
(SOME x, _) => Free (x, map_type T)
| (_, (true, c)) => Const (c, map_type T)
- | (_, (false, c)) => (if NameSpace.is_qualified c then Const else Free) (c, map_type T))
+ | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, map_type T))
| decode (Var (xi, T)) = Var (xi, map_type T)
| decode (t as Bound _) = t;
in decode tm end;
--- a/src/Pure/Thy/thm_deps.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Thy/thm_deps.ML Mon Mar 09 10:10:34 2009 +0100
@@ -20,7 +20,7 @@
fun add_dep ("", _, _) = I
| add_dep (name, _, PBody {thms = thms', ...}) =
let
- val prefix = #1 (Library.split_last (NameSpace.explode name));
+ val prefix = #1 (Library.split_last (Long_Name.explode name));
val session =
(case prefix of
a :: _ =>
@@ -33,7 +33,7 @@
| _ => ["global"]);
val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
val entry =
- {name = NameSpace.base_name name,
+ {name = Long_Name.base_name name,
ID = name,
dir = space_implode "/" (session @ prefix),
unfold = false,
--- a/src/Pure/Thy/thy_output.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML Mon Mar 09 10:10:34 2009 +0100
@@ -11,18 +11,22 @@
val indent: int ref
val source: bool ref
val break: bool ref
- val add_commands: (string * (Args.src -> Toplevel.node option -> string)) list -> unit
+ val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
val defined_command: string -> bool
val defined_option: string -> bool
val print_antiquotations: unit -> unit
val boolean: string -> bool
val integer: string -> int
+ val raw_antiquotation: string -> (Args.src -> Toplevel.state ->
+ Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
+ val antiquotation: string -> (Args.src -> Proof.context ->
+ Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
val args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
- (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.node option -> string
+ (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
datatype markup = Markup | MarkupEnv | Verbatim
val modes: string list ref
- val eval_antiquote: Scan.lexicon -> Toplevel.node option -> SymbolPos.text * Position.T -> string
+ val eval_antiquote: Scan.lexicon -> Toplevel.state -> SymbolPos.text * Position.T -> string
val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
(Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
val str_of_source: Args.src -> string
@@ -57,7 +61,7 @@
local
val global_commands =
- ref (Symtab.empty: (Args.src -> Toplevel.node option -> string) Symtab.table);
+ ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
val global_options =
ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
@@ -81,7 +85,7 @@
NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos)
| SOME f =>
(Position.report (Markup.doc_antiq name) pos;
- (fn node => f src node handle ERROR msg =>
+ (fn state => f src state handle ERROR msg =>
cat_error msg ("The error(s) above occurred in document antiquotation: " ^
quote name ^ Position.str_of pos))))
end;
@@ -127,10 +131,18 @@
fun syntax scan = Args.context_syntax "document antiquotation" scan;
-fun args scan f src node : string =
+fun raw_antiquotation name scan =
+ add_commands [(name, fn src => fn state =>
+ #1 (syntax (scan src state) src (Toplevel.presentation_context_of state NONE)))];
+
+fun antiquotation name scan =
+ raw_antiquotation name (fn src => fn state =>
+ scan src (Toplevel.presentation_context_of state NONE));
+
+fun args scan f src state : string =
let
val loc = if ! locale = "" then NONE else SOME (! locale);
- val (x, ctxt) = syntax scan src (Toplevel.presentation_context node loc);
+ val (x, ctxt) = syntax scan src (Toplevel.presentation_context_of state loc);
in f src ctxt x end;
@@ -153,20 +165,20 @@
val modes = ref ([]: string list);
-fun eval_antiquote lex node (txt, pos) =
+fun eval_antiquote lex state (txt, pos) =
let
fun expand (Antiquote.Text s) = s
| expand (Antiquote.Antiq x) =
let val (opts, src) = Antiquote.read_antiq lex antiq x in
- options opts (fn () => command src node) (); (*preview errors!*)
+ options opts (fn () => command src state) (); (*preview errors!*)
PrintMode.with_modes (! modes @ Latex.modes)
- (Output.no_warnings (options opts (fn () => command src node))) ()
+ (Output.no_warnings (options opts (fn () => command src state))) ()
end
| expand (Antiquote.Open _) = ""
| expand (Antiquote.Close _) = "";
val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
in
- if is_none node andalso exists Antiquote.is_antiq ants then
+ if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
else implode (map expand ants)
end;
@@ -187,9 +199,7 @@
| VerbatimToken of string * Position.T;
fun output_token lex state =
- let
- val eval = eval_antiquote lex (try Toplevel.node_of state)
- in
+ let val eval = eval_antiquote lex state in
fn NoToken => ""
| BasicToken tok => Latex.output_basic tok
| MarkupToken (cmd, txt) => Latex.output_markup cmd (eval txt)
@@ -511,13 +521,13 @@
fun output pretty src ctxt = output_list pretty src ctxt o single;
-fun proof_state node =
- (case Option.map Toplevel.proof_node node of
- SOME (SOME prf) => ProofNode.current prf
+fun proof_state state =
+ (case try Toplevel.proof_of state of
+ SOME prf => prf
| _ => error "No proof state");
-fun output_goals main_goal src node = args (Scan.succeed ()) (output (fn _ => fn _ =>
- Pretty.chunks (Proof.pretty_goals main_goal (proof_state node)))) src node;
+fun output_goals main_goal src state = args (Scan.succeed ()) (output (fn _ => fn _ =>
+ Pretty.chunks (Proof.pretty_goals main_goal (proof_state state)))) src state;
fun ml_val txt = "fn _ => (" ^ txt ^ ");";
fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
--- a/src/Pure/Tools/find_theorems.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML Mon Mar 09 10:10:34 2009 +0100
@@ -279,7 +279,7 @@
val index_ord = option_ord (K EQUAL);
val hidden_ord = bool_ord o pairself NameSpace.is_hidden;
-val qual_ord = int_ord o pairself (length o NameSpace.explode);
+val qual_ord = int_ord o pairself (length o Long_Name.explode);
val txt_ord = int_ord o pairself size;
fun nicer_name (x, i) (y, j) =
--- a/src/Pure/axclass.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/axclass.ML Mon Mar 09 10:10:34 2009 +0100
@@ -158,7 +158,7 @@
(* maintain instances *)
-fun instance_name (a, c) = NameSpace.base_name c ^ "_" ^ NameSpace.base_name a;
+fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
val get_instances = #1 o #2 o AxClassData.get;
val map_instances = AxClassData.map o apsnd o apfst;
@@ -366,7 +366,7 @@
| NONE => error ("Illegal type for instantiation of class parameter: "
^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
val name_inst = instance_name (tyco, class) ^ "_inst";
- val c' = NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco;
+ val c' = Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco;
val T' = Type.strip_sorts T;
in
thy
@@ -390,7 +390,7 @@
val SOME tyco = inst_tyco_of thy (c, T);
val (c', eq) = get_inst_param thy (c, tyco);
val prop = Logic.mk_equals (Const (c', T), t);
- val name' = Thm.def_name_optional (NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco) name;
+ val name' = Thm.def_name_optional (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco) name;
in
thy
|> Thm.add_def false false (Binding.name name', prop)
--- a/src/Pure/codegen.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/codegen.ML Mon Mar 09 10:10:34 2009 +0100
@@ -378,7 +378,7 @@
| (true, "isup") => "" :: check_str zs
| (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs)
| (ys, zs) => implode ys :: check_str zs);
- val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.explode s))
+ val s' = space_implode "_" (maps (check_str o Symbol.explode) (Long_Name.explode s))
in
if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
end;
@@ -388,8 +388,8 @@
fun find_name [] = sys_error "mk_long_id"
| find_name (ys :: yss) =
let
- val s' = NameSpace.implode ys
- val s'' = NameSpace.append module s'
+ val s' = Long_Name.implode ys
+ val s'' = Long_Name.append module s'
in case Symtab.lookup used s'' of
NONE => ((module, s'),
(Symtab.update_new (s, (module, s')) tab,
@@ -397,7 +397,7 @@
| SOME _ => find_name yss
end
in case Symtab.lookup tab s of
- NONE => find_name (Library.suffixes1 (NameSpace.explode s))
+ NONE => find_name (Library.suffixes1 (Long_Name.explode s))
| SOME name => (name, p)
end;
--- a/src/Pure/consts.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/consts.ML Mon Mar 09 10:10:34 2009 +0100
@@ -117,7 +117,7 @@
fun syntax consts (c, mx) =
let
val ({T, authentic, ...}, _) = the_const consts c handle TYPE (msg, _, _) => error msg;
- val c' = if authentic then Syntax.constN ^ c else NameSpace.base_name c;
+ val c' = if authentic then Syntax.constN ^ c else Long_Name.base_name c;
in (c', T, mx) end;
fun syntax_name consts c = #1 (syntax consts (c, NoSyn));
--- a/src/Pure/logic.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/logic.ML Mon Mar 09 10:10:34 2009 +0100
@@ -230,7 +230,7 @@
(* class relations *)
fun name_classrel (c1, c2) =
- NameSpace.base_name c1 ^ "_" ^ NameSpace.base_name c2;
+ Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2;
fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2);
@@ -243,8 +243,8 @@
(* type arities *)
fun name_arities (t, _, S) =
- let val b = NameSpace.base_name t
- in S |> map (fn c => NameSpace.base_name c ^ "_" ^ b) end;
+ let val b = Long_Name.base_name t
+ in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end;
fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
--- a/src/Pure/old_term.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/old_term.ML Mon Mar 09 10:10:34 2009 +0100
@@ -39,7 +39,7 @@
(*Accumulates the names in the term, suppressing duplicates.
Includes Frees and Consts. For choosing unambiguous bound var names.*)
-fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base_name a) bs
+fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
| add_term_names (Free(a,_), bs) = insert (op =) a bs
| add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
| add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
--- a/src/Pure/primitive_defs.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/primitive_defs.ML Mon Mar 09 10:10:34 2009 +0100
@@ -81,7 +81,7 @@
fun mk_defpair (lhs, rhs) =
(case Term.head_of lhs of
Const (name, _) =>
- (NameSpace.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
+ (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
| _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
end;
--- a/src/Pure/sign.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/sign.ML Mon Mar 09 10:10:34 2009 +0100
@@ -355,7 +355,7 @@
fun check_vars (t $ u) = (check_vars t; check_vars u)
| check_vars (Abs (_, _, t)) = check_vars t
| check_vars (Free (x, _)) =
- if NameSpace.is_qualified x then err ("Malformed variable: " ^ quote x) else ()
+ if Long_Name.is_qualified x then err ("Malformed variable: " ^ quote x) else ()
| check_vars (Var (xi as (_, i), _)) =
if i < 0 then err ("Malformed variable: " ^ quote (Term.string_of_vname xi)) else ()
| check_vars _ = ();
--- a/src/Pure/term.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Pure/term.ML Mon Mar 09 10:10:34 2009 +0100
@@ -490,7 +490,7 @@
fun declare_term_names tm =
fold_aterms
- (fn Const (a, _) => Name.declare (NameSpace.base_name a)
+ (fn Const (a, _) => Name.declare (Long_Name.base_name a)
| Free (a, _) => Name.declare a
| _ => I) tm #>
fold_types declare_typ_names tm;
@@ -721,7 +721,7 @@
fun lambda v t =
let val x =
(case v of
- Const (x, _) => NameSpace.base_name x
+ Const (x, _) => Long_Name.base_name x
| Free (x, _) => x
| Var ((x, _), _) => x
| _ => Name.uu)
--- a/src/Tools/code/code_haskell.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Tools/code/code_haskell.ML Mon Mar 09 10:10:34 2009 +0100
@@ -34,7 +34,7 @@
fun pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const
init_syms deresolve is_cons contr_classparam_typs deriving_show =
let
- val deresolve_base = NameSpace.base_name o deresolve;
+ val deresolve_base = Long_Name.base_name o deresolve;
fun class_name class = case syntax_class class
of NONE => deresolve class
| SOME class => class;
@@ -143,7 +143,7 @@
@ str "="
:: str "error"
@@ (str o (fn s => s ^ ";") o ML_Syntax.print_string
- o NameSpace.base_name o NameSpace.qualifier) name
+ o Long_Name.base_name o Long_Name.qualifier) name
)
]
end
@@ -155,7 +155,7 @@
let
val consts = map_filter
(fn c => if (is_some o syntax_const) c
- then NONE else (SOME o NameSpace.base_name o deresolve) c)
+ then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = init_syms
|> Code_Name.intro_vars consts
@@ -255,7 +255,7 @@
let
val (c_inst_name, (_, tys)) = c_inst;
val const = if (is_some o syntax_const) c_inst_name
- then NONE else (SOME o NameSpace.base_name o deresolve) c_inst_name;
+ then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name;
val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
val (vs, rhs) = unfold_abs_pure proto_rhs;
val vars = init_syms
@@ -313,11 +313,11 @@
| Code_Thingol.Classinst _ => pair base;
fun add_stmt' base' = case stmt
of Code_Thingol.Datatypecons _ =>
- cons (name, (NameSpace.append module_name' base', NONE))
+ cons (name, (Long_Name.append module_name' base', NONE))
| Code_Thingol.Classrel _ => I
| Code_Thingol.Classparam _ =>
- cons (name, (NameSpace.append module_name' base', NONE))
- | _ => cons (name, (NameSpace.append module_name' base', SOME stmt));
+ cons (name, (Long_Name.append module_name' base', NONE))
+ | _ => cons (name, (Long_Name.append module_name' base', SOME stmt));
in
Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
(apfst (fold (insert (op = : string * string -> bool)) deps))
@@ -360,7 +360,7 @@
val reserved_names = Code_Name.make_vars reserved_names;
fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
syntax_class syntax_tyco syntax_const reserved_names
- (if qualified then deresolver else NameSpace.base_name o deresolver)
+ (if qualified then deresolver else Long_Name.base_name o deresolver)
is_cons contr_classparam_typs
(if string_classes then deriving_show else K false);
fun pr_module name content =
@@ -379,10 +379,10 @@
|> map_filter (try deresolver);
val qualified = is_none module_name andalso
map deresolver stmt_names @ deps'
- |> map NameSpace.base_name
+ |> map Long_Name.base_name
|> has_duplicates (op =);
val imports = deps'
- |> map NameSpace.qualifier
+ |> map Long_Name.qualifier
|> distinct (op =);
fun pr_import_include (name, _) = str ("import qualified " ^ name ^ ";");
val pr_import_module = str o (if qualified
@@ -413,7 +413,7 @@
val filename = case modlname
of "" => Path.explode "Main.hs"
| _ => (Path.ext "hs" o Path.explode o implode o separate "/"
- o NameSpace.explode) modlname;
+ o Long_Name.explode) modlname;
val pathname = Path.append destination filename;
val _ = File.mkdir (Path.dir pathname);
in File.write pathname
--- a/src/Tools/code/code_ml.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Tools/code/code_ml.ML Mon Mar 09 10:10:34 2009 +0100
@@ -46,8 +46,8 @@
fun pr_sml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
let
val pr_label_classrel = translate_string (fn "." => "__" | c => c)
- o NameSpace.qualifier;
- val pr_label_classparam = NameSpace.base_name o NameSpace.qualifier;
+ o Long_Name.qualifier;
+ val pr_label_classparam = Long_Name.base_name o Long_Name.qualifier;
fun pr_dicts fxy ds =
let
fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_"
@@ -163,7 +163,7 @@
fun pr_stmt (MLExc (name, n)) =
let
val exc_str =
- (ML_Syntax.print_string o NameSpace.base_name o NameSpace.qualifier) name;
+ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name;
in
concat (
str (if n = 0 then "val" else "fun")
@@ -179,7 +179,7 @@
let
val consts = map_filter
(fn c => if (is_some o syntax_const) c
- then NONE else (SOME o NameSpace.base_name o deresolve) c)
+ then NONE else (SOME o Long_Name.base_name o deresolve) c)
(Code_Thingol.fold_constnames (insert (op =)) t []);
val vars = reserved_names
|> Code_Name.intro_vars consts;
@@ -204,7 +204,7 @@
let
val consts = map_filter
(fn c => if (is_some o syntax_const) c
- then NONE else (SOME o NameSpace.base_name o deresolve) c)
+ then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
|> Code_Name.intro_vars consts
@@ -473,7 +473,7 @@
fun pr_stmt (MLExc (name, n)) =
let
val exc_str =
- (ML_Syntax.print_string o NameSpace.base_name o NameSpace.qualifier) name;
+ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name;
in
concat (
str "let"
@@ -488,7 +488,7 @@
let
val consts = map_filter
(fn c => if (is_some o syntax_const) c
- then NONE else (SOME o NameSpace.base_name o deresolve) c)
+ then NONE else (SOME o Long_Name.base_name o deresolve) c)
(Code_Thingol.fold_constnames (insert (op =)) t []);
val vars = reserved_names
|> Code_Name.intro_vars consts;
@@ -508,7 +508,7 @@
let
val consts = map_filter
(fn c => if (is_some o syntax_const) c
- then NONE else (SOME o NameSpace.base_name o deresolve) c)
+ then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
|> Code_Name.intro_vars consts
@@ -524,7 +524,7 @@
let
val consts = map_filter
(fn c => if (is_some o syntax_const) c
- then NONE else (SOME o NameSpace.base_name o deresolve) c)
+ then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
|> Code_Name.intro_vars consts
@@ -552,7 +552,7 @@
let
val consts = map_filter
(fn c => if (is_some o syntax_const) c
- then NONE else (SOME o NameSpace.base_name o deresolve) c)
+ then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames)
(insert (op =)) (map (snd o fst) eqs) []);
val vars = reserved_names
@@ -860,7 +860,7 @@
^ commas (map labelled_name names)
^ "\n"
^ commas module_names);
- val module_name_path = NameSpace.explode module_name;
+ val module_name_path = Long_Name.explode module_name;
fun add_dep name name' =
let
val module_name' = (mk_name_module o fst o Code_Name.dest_name) name';
@@ -868,7 +868,7 @@
map_node module_name_path (Graph.add_edge (name, name'))
else let
val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =)
- (module_name_path, NameSpace.explode module_name');
+ (module_name_path, Long_Name.explode module_name');
in
map_node common
(fn node => Graph.add_edge_acyclic (diff1, diff2) node
@@ -892,7 +892,7 @@
fun deresolver prefix name =
let
val module_name = (fst o Code_Name.dest_name) name;
- val module_name' = (NameSpace.explode o mk_name_module) module_name;
+ val module_name' = (Long_Name.explode o mk_name_module) module_name;
val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
val stmt_name =
nodes
@@ -901,7 +901,7 @@
|> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
| Dummy stmt_name => stmt_name);
in
- NameSpace.implode (remainder @ [stmt_name])
+ Long_Name.implode (remainder @ [stmt_name])
end handle Graph.UNDEF _ =>
error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, nodes) end;
@@ -1011,7 +1011,7 @@
let
val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
val (raw_ml_code, consts_map) = Lazy.force acc_code;
- val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
+ val const'' = Long_Name.append (Long_Name.append struct_name struct_code_name)
((the o AList.lookup (op =) consts_map) const);
val ml_code = if is_first then "\nstructure " ^ struct_code_name
^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n"
--- a/src/Tools/code/code_name.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Tools/code/code_name.ML Mon Mar 09 10:10:34 2009 +0100
@@ -39,7 +39,7 @@
val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
val dest_name =
- apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
+ apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
(** purification **)
@@ -80,7 +80,7 @@
#> Symbol.scanner "Malformed name"
(Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
#> implode
- #> NameSpace.explode
+ #> Long_Name.explode
#> map (purify_name true false);
(*FIMXE non-canonical function treating non-canonical names*)
@@ -101,11 +101,11 @@
fun check_modulename mn =
let
- val mns = NameSpace.explode mn;
+ val mns = Long_Name.explode mn;
val mns' = map (purify_name true false) mns;
in
if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
- ^ "perhaps try " ^ quote (NameSpace.implode mns'))
+ ^ "perhaps try " ^ quote (Long_Name.implode mns'))
end;
@@ -155,11 +155,11 @@
fun mk_alias name = case module_alias name
of SOME name' => name'
| NONE => name
- |> NameSpace.explode
+ |> Long_Name.explode
|> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
- |> NameSpace.implode;
+ |> Long_Name.implode;
fun mk_prefix name = case module_prefix
- of SOME module_prefix => NameSpace.append module_prefix name
+ of SOME module_prefix => Long_Name.append module_prefix name
| NONE => name;
val tab =
Symtab.empty
--- a/src/Tools/code/code_thingol.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/Tools/code/code_thingol.ML Mon Mar 09 10:10:34 2009 +0100
@@ -243,18 +243,18 @@
let
val prefix = get_thyname thy name;
val base = (Code_Name.purify_base true o get_basename) name;
- in NameSpace.append prefix base end;
+ in Long_Name.append prefix base end;
in
-fun namify_class thy = namify thy NameSpace.base_name thyname_of_class;
+fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
fun namify_classrel thy = namify thy (fn (class1, class2) =>
- NameSpace.base_name class2 ^ "_" ^ NameSpace.base_name class1) (fn thy => thyname_of_class thy o fst);
+ Long_Name.base_name class2 ^ "_" ^ Long_Name.base_name class1) (fn thy => thyname_of_class thy o fst);
(*order fits nicely with composed projections*)
fun namify_tyco thy "fun" = "Pure.fun"
- | namify_tyco thy tyco = namify thy NameSpace.base_name thyname_of_tyco tyco;
+ | namify_tyco thy tyco = namify thy Long_Name.base_name thyname_of_tyco tyco;
fun namify_instance thy = namify thy (fn (class, tyco) =>
- NameSpace.base_name class ^ "_" ^ NameSpace.base_name tyco) thyname_of_instance;
-fun namify_const thy = namify thy NameSpace.base_name thyname_of_const;
+ Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance;
+fun namify_const thy = namify thy Long_Name.base_name thyname_of_const;
end; (* local *)
@@ -327,7 +327,7 @@
val suffix_const = "const";
fun add_suffix nsp NONE = NONE
- | add_suffix nsp (SOME name) = SOME (NameSpace.append name nsp);
+ | add_suffix nsp (SOME name) = SOME (Long_Name.append name nsp);
in
--- a/src/ZF/Tools/datatype_package.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/ZF/Tools/datatype_package.ML Mon Mar 09 10:10:34 2009 +0100
@@ -74,7 +74,7 @@
Syntax.string_of_term_global thy t);
val rec_names = map (#1 o dest_Const) rec_hds
- val rec_base_names = map NameSpace.base_name rec_names
+ val rec_base_names = map Long_Name.base_name rec_names
val big_rec_base_name = space_implode "_" rec_base_names
val thy_path = thy |> Sign.add_path big_rec_base_name
--- a/src/ZF/Tools/induct_tacs.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Mon Mar 09 10:10:34 2009 +0100
@@ -157,7 +157,7 @@
in
thy
- |> Sign.add_path (NameSpace.base_name big_rec_name)
+ |> Sign.add_path (Long_Name.base_name big_rec_name)
|> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
|> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
|> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
--- a/src/ZF/Tools/inductive_package.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML Mon Mar 09 10:10:34 2009 +0100
@@ -80,7 +80,7 @@
val rec_names = map (#1 o dest_Const) rec_hds
and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
- val rec_base_names = map NameSpace.base_name rec_names;
+ val rec_base_names = map Long_Name.base_name rec_names;
val dummy = assert_all Syntax.is_identifier rec_base_names
(fn a => "Base name of recursive set not an identifier: " ^ a);
@@ -377,7 +377,7 @@
mutual recursion to invariably be a disjoint sum.*)
fun mk_predpair rec_tm =
let val rec_name = (#1 o dest_Const o head_of) rec_tm
- val pfree = Free(pred_name ^ "_" ^ NameSpace.base_name rec_name,
+ val pfree = Free(pred_name ^ "_" ^ Long_Name.base_name rec_name,
elem_factors ---> FOLogic.oT)
val qconcl =
List.foldr FOLogic.mk_all
--- a/src/ZF/Tools/primrec_package.ML Mon Mar 09 09:37:33 2009 +0100
+++ b/src/ZF/Tools/primrec_package.ML Mon Mar 09 10:10:34 2009 +0100
@@ -139,7 +139,7 @@
(** make definition **)
(*the recursive argument*)
- val rec_arg = Free (Name.variant (map #1 (ls@rs)) (NameSpace.base_name big_rec_name),
+ val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Long_Name.base_name big_rec_name),
Ind_Syntax.iT)
val def_tm = Logic.mk_equals
@@ -153,7 +153,7 @@
writeln ("primrec def:\n" ^
Syntax.string_of_term_global thy def_tm)
else();
- (NameSpace.base_name fname ^ "_" ^ NameSpace.base_name big_rec_name ^ "_def",
+ (Long_Name.base_name fname ^ "_" ^ Long_Name.base_name big_rec_name ^ "_def",
def_tm)
end;
@@ -168,7 +168,7 @@
val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
val ([def_thm], thy1) = thy
- |> Sign.add_path (NameSpace.base_name fname)
+ |> Sign.add_path (Long_Name.base_name fname)
|> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)];
val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)