--- a/.hgignore Tue Dec 02 17:50:25 2008 +0100
+++ b/.hgignore Tue Dec 02 17:50:39 2008 +0100
@@ -1,7 +1,6 @@
syntax: glob
*~
-*.dvi
*.class
*.jar
.DS_Store
@@ -11,4 +10,15 @@
^heaps/
^browser_info/
+^doc-src/.*\.aux
+^doc-src/.*\.bbl
+^doc-src/.*\.blg
+^doc-src/.*\.dvi
+^doc-src/.*\.idx
+^doc-src/.*\.ind
+^doc-src/.*\.log
+^doc-src/.*\.out
+^doc-src/.*\.rai
+^doc-src/.*\.rao
+^doc-src/.*\.toc
--- a/src/FOL/ex/NewLocaleTest.thy Tue Dec 02 17:50:25 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy Tue Dec 02 17:50:39 2008 +0100
@@ -157,11 +157,6 @@
show ?t by (rule x [OF `?a`])
qed
-lemma
- assumes "P <-> P" (is "?p <-> _")
- shows "?p <-> ?p"
- .
-
text {* Interpretation between locales: sublocales *}
--- a/src/HOL/Complex/Complex.thy Tue Dec 02 17:50:25 2008 +0100
+++ b/src/HOL/Complex/Complex.thy Tue Dec 02 17:50:39 2008 +0100
@@ -8,7 +8,7 @@
header {* Complex Numbers: Rectangular and Polar Representations *}
theory Complex
-imports "../Real/Real" "../Hyperreal/Transcendental"
+imports "../Hyperreal/Transcendental"
begin
datatype complex = Complex real real
--- a/src/HOL/Complex/Complex_Main.thy Tue Dec 02 17:50:25 2008 +0100
+++ b/src/HOL/Complex/Complex_Main.thy Tue Dec 02 17:50:39 2008 +0100
@@ -9,6 +9,8 @@
theory Complex_Main
imports
"../Main"
+ "../Real/ContNotDenum"
+ "../Real/Real"
Fundamental_Theorem_Algebra
"../Hyperreal/Log"
"../Hyperreal/Ln"
--- a/src/HOL/Hyperreal/Fact.thy Tue Dec 02 17:50:25 2008 +0100
+++ b/src/HOL/Hyperreal/Fact.thy Tue Dec 02 17:50:39 2008 +0100
@@ -7,7 +7,7 @@
header{*Factorial Function*}
theory Fact
-imports "../Real/Real"
+imports "../Real/RealDef"
begin
consts fact :: "nat => nat"
--- a/src/HOL/Hyperreal/SEQ.thy Tue Dec 02 17:50:25 2008 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy Tue Dec 02 17:50:39 2008 +0100
@@ -9,7 +9,7 @@
header {* Sequences and Convergence *}
theory SEQ
-imports "../Real/Real" "../Real/ContNotDenum"
+imports "../Real/RealVector" "../Real/RComplete"
begin
definition
--- a/src/HOL/Library/Executable_Set.thy Tue Dec 02 17:50:25 2008 +0100
+++ b/src/HOL/Library/Executable_Set.thy Tue Dec 02 17:50:39 2008 +0100
@@ -16,7 +16,7 @@
declare subset_def [symmetric, code unfold]
-lemma "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
+lemma [code]: "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
unfolding subset_def subset_eq ..
definition is_empty :: "'a set \<Rightarrow> bool" where
@@ -32,8 +32,7 @@
"a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
unfolding bex_triv_one_point1 ..
-definition
- filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
"filter_set P xs = {x\<in>xs. P x}"
--- a/src/HOL/Real/PReal.thy Tue Dec 02 17:50:25 2008 +0100
+++ b/src/HOL/Real/PReal.thy Tue Dec 02 17:50:39 2008 +0100
@@ -1,5 +1,4 @@
(* Title : PReal.thy
- ID : $Id$
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Description : The positive reals as Dedekind sections of positive
@@ -10,7 +9,7 @@
header {* Positive real numbers *}
theory PReal
-imports Rational Dense_Linear_Order
+imports Rational "~~/src/HOL/Library/Dense_Linear_Order"
begin
text{*Could be generalized and moved to @{text Ring_and_Field}*}
--- a/src/HOL/Tools/inductive_package.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/HOL/Tools/inductive_package.ML Tue Dec 02 17:50:39 2008 +0100
@@ -638,8 +638,8 @@
(* add definiton of recursive predicates to theory *)
val rec_name =
- if Name.is_nothing alt_name then
- Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
+ if Binding.is_nothing alt_name then
+ Binding.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
else alt_name;
val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
--- a/src/HOL/Tools/inductive_set_package.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Tue Dec 02 17:50:39 2008 +0100
@@ -499,8 +499,8 @@
(* convert theorems to set notation *)
val rec_name =
- if Name.is_nothing alt_name then
- Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
+ if Binding.is_nothing alt_name then
+ Binding.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
else alt_name;
val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn; (* FIXME *)
val (intr_names, intr_atts) = split_list (map fst intros);
--- a/src/Pure/General/ROOT.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/General/ROOT.ML Tue Dec 02 17:50:39 2008 +0100
@@ -27,6 +27,7 @@
use "ord_list.ML";
use "balanced_tree.ML";
use "graph.ML";
+use "binding.ML";
use "name_space.ML";
use "lazy.ML";
use "path.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/binding.ML Tue Dec 02 17:50:39 2008 +0100
@@ -0,0 +1,75 @@
+(* Title: Pure/General/binding.ML
+ Author: Florian Haftmann, TU Muenchen
+
+Structured name bindings.
+*)
+
+signature BASIC_BINDING =
+sig
+ val long_names: bool ref
+ val short_names: bool ref
+ val unique_names: bool ref
+end;
+
+signature BINDING =
+sig
+ include BASIC_BINDING
+ type T
+ val binding_pos: string * Position.T -> T
+ val binding: string -> T
+ val no_binding: T
+ val dest_binding: T -> (string * bool) list * string
+ val is_nothing: T -> bool
+ val pos_of: T -> Position.T
+
+ val map_binding: ((string * bool) list * string -> (string * bool) list * string)
+ -> T -> T
+ val add_prefix: bool -> string -> T -> T
+ val map_prefix: ((string * bool) list -> T -> T) -> T -> T
+ val display: T -> string
+end
+
+structure Binding : BINDING =
+struct
+
+(** global flags **)
+
+val long_names = ref false;
+val short_names = ref false;
+val unique_names = ref true;
+
+
+(** binding representation **)
+
+datatype T = Binding of ((string * bool) list * string) * Position.T;
+ (* (prefix components (with mandatory flag), base name, position) *)
+
+fun binding_pos (name, pos) = Binding (([], name), pos);
+fun binding name = binding_pos (name, Position.none);
+val no_binding = binding "";
+
+fun pos_of (Binding (_, pos)) = pos;
+fun dest_binding (Binding (prefix_name, _)) = prefix_name;
+
+fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
+
+fun is_nothing (Binding ((_, name), _)) = name = "";
+
+fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
+ else (map_binding o apfst) (cons (prfx, sticky)) b;
+
+fun map_prefix f (Binding ((prefix, name), pos)) =
+ f prefix (binding_pos (name, pos));
+
+fun display (Binding ((prefix, name), _)) =
+ let
+ fun mk_prefix (prfx, true) = prfx
+ | mk_prefix (prfx, false) = enclose "(" ")" prfx
+ in if not (! long_names) orelse null prefix orelse name = "" then name
+ else space_implode "." (map mk_prefix prefix) ^ ":" ^ name
+ end;
+
+end;
+
+structure Basic_Binding : BASIC_BINDING = Binding;
+open Basic_Binding;
--- a/src/Pure/General/name_space.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/General/name_space.ML Tue Dec 02 17:50:39 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/name_space.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Generic name spaces with declared and hidden entries. Unknown names
@@ -9,29 +8,9 @@
type bstring = string; (*names to be bound*)
type xstring = string; (*external names*)
-signature BASIC_NAME_SPACE =
-sig
- val long_names: bool ref
- val short_names: bool ref
- val unique_names: bool ref
-end;
-
-signature NAME_BINDING =
-sig
- type binding
- val binding_pos: string * Position.T -> binding
- val binding: string -> binding
- val no_binding: binding
- val dest_binding: binding -> (string * bool) list * string
- val is_nothing: binding -> bool
- val pos_of: binding -> Position.T
- val map_binding: ((string * bool) list * string -> (string * bool) list * string)
- -> binding -> binding
-end
-
signature NAME_SPACE =
sig
- include BASIC_NAME_SPACE
+ include BASIC_BINDING
val hidden: string -> string
val is_hidden: string -> bool
val separator: string (*single char*)
@@ -60,14 +39,13 @@
val no_base_names: naming -> naming
val qualified_names: naming -> naming
val sticky_prefix: string -> naming -> naming
- include NAME_BINDING
- val full_binding: naming -> binding -> string
- val declare_binding: naming -> binding -> T -> string * T
+ val full_binding: naming -> Binding.T -> string
+ val declare_binding: naming -> Binding.T -> T -> string * T
type 'a table = T * 'a Symtab.table
val empty_table: 'a table
- val table_declare: naming -> binding * 'a
+ val table_declare: naming -> Binding.T * 'a
-> 'a table -> string * 'a table (*exception Symtab.DUP*)
- val table_declare_permissive: naming -> binding * 'a
+ val table_declare_permissive: naming -> Binding.T * 'a
-> 'a table -> string * 'a table
val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
@@ -78,6 +56,9 @@
structure NameSpace: NAME_SPACE =
struct
+open Basic_Binding;
+
+
(** long identifiers **)
fun hidden name = "??." ^ name;
@@ -170,10 +151,6 @@
fun intern space xname = #1 (lookup space xname);
-val long_names = ref false;
-val short_names = ref false;
-val unique_names = ref true;
-
fun extern space name =
let
fun valid unique xname =
@@ -241,23 +218,6 @@
-(** generic name bindings **)
-
-datatype binding = Binding of ((string * bool) list * string) * Position.T;
-
-fun binding_pos (name, pos) = Binding (([], name), pos);
-fun binding name = binding_pos (name, Position.none);
-val no_binding = binding "";
-
-fun pos_of (Binding (_, pos)) = pos;
-fun dest_binding (Binding (prefix_name, _)) = prefix_name;
-
-fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
-
-fun is_nothing (Binding ((_, name), _)) = name = "";
-
-
-
(** naming contexts **)
(* datatype naming *)
@@ -321,8 +281,9 @@
val (accs, accs') = pairself (map implode_name) (accesses naming names);
in space |> fold (add_name name) accs |> put_accesses name accs' end;
-fun declare_binding bnaming (Binding ((prefix, bname), _)) =
+fun declare_binding bnaming b =
let
+ val (prefix, bname) = Binding.dest_binding b;
val naming = apply_prefix prefix bnaming;
val name = full naming bname;
in declare naming name #> pair name end;
@@ -343,8 +304,9 @@
fun table_declare naming = gen_table_declare Symtab.update_new naming;
fun table_declare_permissive naming = gen_table_declare Symtab.update naming;
-fun full_binding naming (Binding ((prefix, bname), _)) =
- full (apply_prefix prefix naming) bname;
+fun full_binding naming b =
+ let val (prefix, bname) = Binding.dest_binding b
+ in full (apply_prefix prefix naming) bname end;
fun extend_table naming bentries (space, tab) =
let val entries = map (apfst (full naming)) bentries
@@ -366,6 +328,3 @@
val explode = explode_name;
end;
-
-structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
-open BasicNameSpace;
--- a/src/Pure/Isar/args.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/Isar/args.ML Tue Dec 02 17:50:39 2008 +0100
@@ -171,7 +171,7 @@
val name_source_position = named >> T.source_position_of;
val name = named >> T.content_of;
-val binding = P.position name >> Name.binding_pos;
+val binding = P.position name >> Binding.binding_pos;
val alt_name = alt_string >> T.content_of;
val symbol = symbolic >> T.content_of;
val liberal_name = symbol || name;
--- a/src/Pure/Isar/class.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/Isar/class.ML Tue Dec 02 17:50:39 2008 +0100
@@ -78,7 +78,7 @@
val class_prefix = Logic.const_of_class o Sign.base_name;
fun class_name_morphism class =
- Name.map_prefix (K (Name.add_prefix false (class_prefix class)));
+ Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
fun activate_class_morphism thy class inst morphism =
Locale.get_interpret_morph thy (class_name_morphism class) (class, "") morphism class inst;
--- a/src/Pure/Isar/expression.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/Isar/expression.ML Tue Dec 02 17:50:39 2008 +0100
@@ -304,12 +304,10 @@
(* Type inference *)
val (inst_cs' :: css', ctxt') =
(fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt;
- (* Re-check to resolve bindings, elements and conclusion only *)
- val (css'', _) = (fold_burrow o fold_burrow) check css' ctxt';
- val (elem_css'', [concl_cs'']) = chop (length elem_css) css'';
+ val (elem_css', [concl_cs']) = chop (length elem_css) css';
in
- (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css''),
- concl_cs'', ctxt')
+ (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css'),
+ concl_cs', ctxt')
end;
end;
--- a/src/Pure/Isar/locale.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/Isar/locale.ML Tue Dec 02 17:50:39 2008 +0100
@@ -92,8 +92,8 @@
(* Storing results *)
val local_note_qualified: string ->
- (Name.binding * attribute list) * (thm list * attribute list) list ->
- Proof.context -> (string * thm list) * Proof.context
+ ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
+ Proof.context -> (string * thm list) list * Proof.context
val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
Proof.context -> Proof.context
val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
@@ -134,18 +134,18 @@
fun merge_alists eq xs = merge_lists (eq_fst eq) xs;
-(* auxiliary: noting with structured name bindings *)
-
-fun global_note_qualified kind ((b, atts), facts_atts_s) thy =
+(* auxiliary: noting name bindings with qualified base names *)
+
+fun global_note_qualified kind facts thy =
thy
|> Sign.qualified_names
- |> yield_singleton (PureThy.note_thmss kind) ((b, atts), facts_atts_s)
+ |> PureThy.note_thmss kind facts
||> Sign.restore_naming thy;
-fun local_note_qualified kind ((b, atts), facts_atts_s) ctxt =
+fun local_note_qualified kind facts ctxt =
ctxt
|> ProofContext.qualified_names
- |> yield_singleton (ProofContext.note_thmss_i kind) ((b, atts), facts_atts_s)
+ |> ProofContext.note_thmss_i kind facts
||> ProofContext.restore_naming ctxt;
@@ -947,8 +947,8 @@
val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
val (lprfx, pprfx) = param_prefix name params;
- val add_prefices = pprfx <> "" ? Name.add_prefix false pprfx
- #> Name.add_prefix false lprfx;
+ val add_prefices = pprfx <> "" ? Binding.add_prefix false pprfx
+ #> Binding.add_prefix false lprfx;
val elem_morphism =
Element.rename_morphism ren $>
Morphism.name_morphism add_prefices $>
@@ -1010,7 +1010,7 @@
| activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) =
let
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
- val (res, ctxt') = ctxt |> fold_map (local_note_qualified kind) facts';
+ val (res, ctxt') = ctxt |> local_note_qualified kind facts';
in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end;
fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
@@ -1634,10 +1634,10 @@
fun name_morph phi_name (lprfx, pprfx) b =
b
- |> (if not (Name.is_nothing b) andalso pprfx <> ""
- then Name.add_prefix false pprfx else I)
- |> (if not (Name.is_nothing b)
- then Name.add_prefix false lprfx else I)
+ |> (if not (Binding.is_nothing b) andalso pprfx <> ""
+ then Binding.add_prefix false pprfx else I)
+ |> (if not (Binding.is_nothing b)
+ then Binding.add_prefix false lprfx else I)
|> phi_name;
fun inst_morph thy phi_name param_prfx insts prems eqns export =
@@ -1696,7 +1696,8 @@
(Attrib.attribute_i thy) insts prems eqns exp;
in
thy
- |> fold (snd oo global_note_qualified kind) args'
+ |> global_note_qualified kind args'
+ |> snd
end;
in fold activate regs thy end;
@@ -2106,7 +2107,8 @@
(attrib thy_ctxt) insts prems eqns exp;
in
thy_ctxt
- |> fold (snd oo note kind) facts'
+ |> note kind facts'
+ |> snd
end
| activate_elem _ _ _ _ _ _ _ thy_ctxt = thy_ctxt;
@@ -2128,7 +2130,7 @@
in
thy_ctxt''
(* add equations as lemmas to context *)
- |> (fold2 o fold2) (fn attn => fn thm => snd o note Thm.lemmaK
+ |> (fold2 o fold2) (fn attn => fn thm => snd o yield_singleton (note Thm.lemmaK)
((apsnd o map) (attrib thy_ctxt'') attn, [([Element.conclude_witness thm], [])]))
(unflat eq_thms eq_attns) eq_thms
(* add interpreted facts *)
@@ -2383,7 +2385,8 @@
|> (map o apfst o apfst) (name_morph phi_name param_prfx);
in
thy
- |> fold (snd oo global_note_qualified kind) facts'
+ |> global_note_qualified kind facts'
+ |> snd
end
| activate_elem _ _ thy = thy;
@@ -2439,11 +2442,11 @@
end;
fun standard_name_morph interp_prfx b =
- if Name.is_nothing b then b
- else Name.map_prefix (fn ((lprfx, _) :: pprfx) =>
- fold (Name.add_prefix false o fst) pprfx
- #> interp_prfx <> "" ? Name.add_prefix true interp_prfx
- #> Name.add_prefix false lprfx
+ if Binding.is_nothing b then b
+ else Binding.map_prefix (fn ((lprfx, _) :: pprfx) =>
+ fold (Binding.add_prefix false o fst) pprfx
+ #> interp_prfx <> "" ? Binding.add_prefix true interp_prfx
+ #> Binding.add_prefix false lprfx
) b;
in
--- a/src/Pure/Isar/new_locale.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML Tue Dec 02 17:50:39 2008 +0100
@@ -295,7 +295,7 @@
| init_elem (Notes (kind, facts)) ctxt =
let
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
- in fold (fn args => Locale.local_note_qualified kind args #> snd) facts' ctxt end
+ in Locale.local_note_qualified kind facts' ctxt |> snd end
fun cons_elem false (Notes notes) elems = elems
| cons_elem _ elem elems = elem :: elems
--- a/src/Pure/Isar/outer_parse.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/Isar/outer_parse.ML Tue Dec 02 17:50:39 2008 +0100
@@ -228,7 +228,7 @@
(* names and text *)
val name = group "name declaration" (short_ident || sym_ident || string || number);
-val binding = position name >> Name.binding_pos;
+val binding = position name >> Binding.binding_pos;
val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
val path = group "file name/path specification" name >> Path.explode;
--- a/src/Pure/Isar/proof_context.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML Tue Dec 02 17:50:39 2008 +0100
@@ -971,7 +971,7 @@
fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
let
- val pos = Name.pos_of b;
+ val pos = Binding.pos_of b;
val name = full_binding ctxt b;
val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
@@ -1128,7 +1128,7 @@
|> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
|-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
- ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Name.pos_of b));
+ ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
in (xs', ctxt'') end;
in
--- a/src/Pure/Isar/specification.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/Isar/specification.ML Tue Dec 02 17:50:39 2008 +0100
@@ -190,7 +190,7 @@
val y = Name.name_of b;
val _ = x = y orelse
error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
- Position.str_of (Name.pos_of b));
+ Position.str_of (Binding.pos_of b));
in (b, mx) end);
val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
(var, ((Name.map_name (suffix "_raw") name, []), rhs));
@@ -223,7 +223,7 @@
val y = Name.name_of b;
val _ = x = y orelse
error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
- Position.str_of (Name.pos_of b));
+ Position.str_of (Binding.pos_of b));
in (b, mx) end);
val lthy' = lthy
|> ProofContext.set_syntax_mode mode (* FIXME ?!? *)
@@ -348,7 +348,7 @@
lthy
|> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
|> (fn (res, lthy') =>
- if Name.is_nothing name andalso null atts then
+ if Binding.is_nothing name andalso null atts then
(ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
else
let
--- a/src/Pure/Isar/theory_target.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML Tue Dec 02 17:50:39 2008 +0100
@@ -201,7 +201,7 @@
val arg = (b', Term.close_schematic_term rhs');
val similar_body = Type.similar_types (rhs, rhs');
(* FIXME workaround based on educated guess *)
- val (prefix', _) = Name.dest_binding b';
+ val (prefix', _) = Binding.dest_binding b';
val class_global = Name.name_of b = Name.name_of b'
andalso not (null prefix')
andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
--- a/src/Pure/facts.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/facts.ML Tue Dec 02 17:50:39 2008 +0100
@@ -192,7 +192,7 @@
fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
let
- val (name, facts') = if Name.is_nothing b then ("", facts)
+ val (name, facts') = if Binding.is_nothing b then ("", facts)
else let
val (space, tab) = facts;
val (name, space') = NameSpace.declare_binding naming b space;
--- a/src/Pure/name.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/name.ML Tue Dec 02 17:50:39 2008 +0100
@@ -29,20 +29,16 @@
val variant_list: string list -> string list -> string list
val variant: string list -> string -> string
- include NAME_BINDING
- val add_prefix: bool -> string -> binding -> binding
- val map_prefix: ((string * bool) list -> binding -> binding) -> binding -> binding
- val name_of: binding -> string (*FIMXE legacy*)
- val map_name: (string -> string) -> binding -> binding (*FIMXE legacy*)
- val qualified: string -> binding -> binding (*FIMXE legacy*)
- val display: binding -> string
+ include BINDING
+ type binding = Binding.T
+ val name_of: Binding.T -> string (*FIMXE legacy*)
+ val map_name: (string -> string) -> Binding.T -> Binding.T (*FIMXE legacy*)
+ val qualified: string -> Binding.T -> Binding.T (*FIMXE legacy*)
end;
structure Name: NAME =
struct
-open NameSpace;
-
(** common defaults **)
val uu = "uu";
@@ -152,27 +148,13 @@
(** generic name bindings **)
-fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
- else (map_binding o apfst) (cons (prfx, sticky)) b;
+open Binding;
+
+type binding = Binding.T;
val prefix_of = fst o dest_binding;
val name_of = snd o dest_binding;
val map_name = map_binding o apsnd;
val qualified = map_name o NameSpace.qualified;
-fun map_prefix f b =
- let
- val (prefix, name) = dest_binding b;
- val pos = pos_of b;
- in f prefix (binding_pos (name, pos)) end;
-
-fun display b =
- let
- val (prefix, name) = dest_binding b
- fun mk_prefix (prfx, true) = prfx
- | mk_prefix (prfx, false) = enclose "(" ")" prfx
- in if not (! NameSpace.long_names) orelse null prefix orelse name = "" then name
- else NameSpace.implode (map mk_prefix prefix) ^ ":" ^ name
- end;
-
end;
--- a/src/Pure/pure_thy.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/pure_thy.ML Tue Dec 02 17:50:39 2008 +0100
@@ -144,7 +144,7 @@
(FactsData.map (apsnd (fold (cons o lazy_proof) thms)) thy, thms);
fun enter_thms pre_name post_name app_att (b, thms) thy =
- if Name.is_nothing b
+ if Binding.is_nothing b
then swap (enter_proofs (app_att (thy, thms)))
else let
val naming = Sign.naming_of thy;
@@ -198,7 +198,7 @@
fun gen_note_thmss tag = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
let
- val pos = Name.pos_of b;
+ val pos = Binding.pos_of b;
val name = Sign.full_binding thy b;
val _ = Position.report (Markup.fact_decl name) pos;
--- a/src/Pure/sign.ML Tue Dec 02 17:50:25 2008 +0100
+++ b/src/Pure/sign.ML Tue Dec 02 17:50:39 2008 +0100
@@ -535,7 +535,7 @@
fun declare_const tags ((b, T), mx) thy =
let
- val pos = Name.pos_of b;
+ val pos = Binding.pos_of b;
val tags' = Position.default_properties pos tags;
val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags' [(b, T, mx)] thy;
val _ = Position.report (Markup.const_decl c) pos;