# HG changeset patch # User haftmann # Date 1236589834 -3600 # Node ID 50eec112ca1c53bfdd5b6fd02e40f70ae2f20241 # Parent ffdd7a1f1ff0200ab665b0bd0deccf71bde74356# Parent 1ae7b86638ad279855ae61881a0a075f59a64459 merged diff -r 1ae7b86638ad -r 50eec112ca1c doc-src/IsarImplementation/Thy/Prelim.thy --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c doc-src/IsarImplementation/Thy/document/Prelim.tex --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c doc-src/antiquote_setup.ML --- 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" @ diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Algebra/Ideal.thy --- 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 \ 'a set \ 'a set" ("Idl\ _" [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: diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Algebra/Lattice.thy --- 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 \ carrier L & g \ A & (ALL x : A. x \ g)" -text {* Could weaken these to @{term [locale=weak_partial_order] "l \ carrier L \ l - .\ A"} and @{term [locale=weak_partial_order] "g \ carrier L \ g .\ A"}. *} +text (in weak_partial_order) {* Could weaken these to @{term "l \ carrier L \ l + .\ A"} and @{term "g \ carrier L \ g .\ A"}. *} lemma least_closed [intro, simp]: "least L l A ==> l \ carrier L" @@ -306,8 +306,8 @@ "[| x .= x'; x \ carrier L; x' \ 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'" diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Algebra/UnivPoly.thy --- 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 \ k \\<^bsub>P\<^esub> monom P \ 1 = monom P \ 1 \\<^bsub>P\<^esub> monom P \ k" unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] .. diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Docs/MainDoc.thy --- 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 xx. x < y \ P"}\\ @{term"ALL x>=y. P"} & @{term[source]"\x. x \ y \ P"}\\ @{term"ALL x>y. P"} & @{term[source]"\x. x > y \ P"}\\ +\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\"} instead of @{text"\"}}\\ @{term"LEAST x. P"} & @{term[source]"Least (\x. P)"}\\ \end{supertabular} -Similar for @{text"\"} instead of @{text"\"}. - \section{Set} Sets are predicates: @{text[source]"'a set = 'a \ 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\'a set\'a set"}\\ @{const Collect} & @{term_type_only Collect "('a\bool)\'a set"}\\ -@{const "op :"} & @{term_type_only "op :" "'a\'a set\bool"}\\ -@{const "op Un"} & @{term_type_only "op Un" "'a set\'a set \ 'a set"}\\ -@{const "op Int"} & @{term_type_only "op Int" "'a set\'a set \ 'a set"}\\ +@{const "op :"} & @{term_type_only "op :" "'a\'a set\bool"} \qquad(\textsc{ascii} @{text":"})\\ +@{const Set.Un} & @{term_type_only Set.Un "'a set\'a set \ 'a set"} \qquad(\textsc{ascii} @{text"Un"})\\ +@{const Set.Int} & @{term_type_only Set.Int "'a set\'a set \ 'a set"} \qquad(\textsc{ascii} @{text"Int"})\\ @{const UNION} & @{term_type_only UNION "'a set\('a \ 'b set) \ 'b set"}\\ @{const INTER} & @{term_type_only INTER "'a set\('a \ 'b set) \ 'b set"}\\ @{const Union} & @{term_type_only Union "'a set set\'a set"}\\ @@ -112,10 +111,10 @@ @{term[source]"A \ B"} & @{term[source]"B \ A"}\\ @{term[source]"A \ B"} & @{term[source]"B < A"}\\ @{term"{x. P}"} & @{term[source]"Collect(\x. P)"}\\ -@{term"UN x:I. A"} & @{term[source]"UNION I (\x. A)"}\\ -@{term"UN x. A"} & @{term[source]"UNION UNIV (\x. A)"}\\ -@{term"INT x:I. A"} & @{term[source]"INTER I (\x. A)"}\\ -@{term"INT x. A"} & @{term[source]"INTER UNIV (\x. A)"}\\ +@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\x. A)"}\\ +@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\x. A)"}\\ +@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\x. A)"}\\ +@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\x. A)"}\\ @{term"ALL x:A. P"} & @{term[source]"Ball A (\x. P)"}\\ @{term"EX x:A. P"} & @{term[source]"Bex A (\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 \ 'a set"}\\ +@{const atMost} & @{term_type_only atMost "'a::ord \ 'a set"}\\ +@{const greaterThan} & @{term_type_only greaterThan "'a::ord \ 'a set"}\\ +@{const atLeast} & @{term_type_only atLeast "'a::ord \ 'a set"}\\ +@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \ 'a \ 'a set"}\\ +@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \ 'a \ 'a set"}\\ +@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \ 'a \ 'a set"}\\ +@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \ 'a \ '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] "\ i \ {..n}. A"}\\ +@{term[mode=xsymbols] "UN i:{..n}. A"} & @{term[source] "\ i \ {..n}. A"}\\ +@{term[mode=xsymbols] "UN i:{.. i \ {.."} instead of @{text"\"}}\\ @{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\x. t) {a..b}"}\\ +@{term "setsum (%x. t) {a..x. t) {a.."} instead of @{text"\"}}\\ \end{supertabular} ??????? diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Import/hol4rews.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Library/normarith.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Nominal/nominal_fresh_fun.ML --- 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 = diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Nominal/nominal_inductive.ML --- 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; diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Nominal/nominal_inductive2.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Nominal/nominal_package.ML --- 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)); diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Nominal/nominal_permeq.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Nominal/nominal_primrec.ML --- 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'); diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Nominal/nominal_thmdecls.ML --- 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)] diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/SetInterval.thy --- 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\ _\_./ _)" 10) "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10) "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10) "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10) -syntax (xsymbols) +syntax (latex output) "@UNION_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10) "@UNION_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00_ < _)/ _)" 10) "@INTER_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10) diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Statespace/state_fun.ML --- 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) "" diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Statespace/state_space.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/TFL/post.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/TFL/tfl.ML --- 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} diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/datatype_abs_proofs.ML --- 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))) ))); diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/datatype_aux.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/datatype_package.ML --- 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, diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/datatype_prop.ML --- 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; diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/datatype_realizer.ML --- 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) $ diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/datatype_rep_proofs.ML --- 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') = diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/function_package/fundef_package.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/function_package/size.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/inductive_package.ML --- 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)), diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/inductive_realizer.ML --- 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; diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/metis_tools.ML --- 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); diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/old_primrec_package.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/primrec_package.ML --- 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; diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/recdef_package.ML --- 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 ^ " ..."); diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/record_package.ML --- 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*) diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/res_atp.ML --- 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; diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/res_axioms.ML --- 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); diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/Tools/specification_package.ML --- 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" diff -r 1ae7b86638ad -r 50eec112ca1c src/HOL/ex/Quickcheck_Generators.thy --- 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, diff -r 1ae7b86638ad -r 50eec112ca1c src/HOLCF/Tools/domain/domain_axioms.ML --- 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')); diff -r 1ae7b86638ad -r 50eec112ca1c src/HOLCF/Tools/domain/domain_extender.ML --- 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; diff -r 1ae7b86638ad -r 50eec112ca1c src/HOLCF/Tools/domain/domain_syntax.ML --- 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); diff -r 1ae7b86638ad -r 50eec112ca1c src/HOLCF/Tools/domain/domain_theorems.ML --- 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] ), diff -r 1ae7b86638ad -r 50eec112ca1c src/HOLCF/Tools/fixrec_package.ML --- 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) diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/General/ROOT.ML --- 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"; diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/General/binding.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)); diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/General/long_name.ML --- /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; + diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/General/name_space.ML --- 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; diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/IsaMakefile --- 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 \ diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Isar/class_target.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 diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Isar/element.ML --- 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 = diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Isar/isar_cmd.ML --- 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; diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Isar/proof_context.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Isar/proof_display.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Isar/rule_cases.ML --- 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); diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Isar/theory_target.ML --- 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, diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Isar/toplevel.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/ML/ml_antiquote.ML --- 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); diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Proof/extraction.ML --- 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); diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Proof/proof_syntax.ML --- 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 = diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/ProofGeneral/proof_general_pgip.ML --- 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) diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Syntax/syntax.ML --- 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); diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Syntax/type_ext.ML --- 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; diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Thy/thm_deps.ML --- 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, diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Thy/thy_output.ML --- 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;"; diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/Tools/find_theorems.ML --- 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) = diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/axclass.ML --- 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) diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/codegen.ML --- 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; diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/consts.ML --- 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)); diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/logic.ML --- 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])); diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/old_term.ML --- 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) diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/primitive_defs.ML --- 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; diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/sign.ML --- 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 _ = (); diff -r 1ae7b86638ad -r 50eec112ca1c src/Pure/term.ML --- 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) diff -r 1ae7b86638ad -r 50eec112ca1c src/Tools/code/code_haskell.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/Tools/code/code_ml.ML --- 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" diff -r 1ae7b86638ad -r 50eec112ca1c src/Tools/code/code_name.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/Tools/code/code_thingol.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/ZF/Tools/datatype_package.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/ZF/Tools/induct_tacs.ML --- 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)) diff -r 1ae7b86638ad -r 50eec112ca1c src/ZF/Tools/inductive_package.ML --- 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 diff -r 1ae7b86638ad -r 50eec112ca1c src/ZF/Tools/primrec_package.ML --- 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)