# HG changeset patch # User wenzelm # Date 1117533203 -7200 # Node ID afd2d32c7d94baa24bb297f6e52e5147f546affe # Parent e1b85512d87d7f7d497877189e44e784476e40c5 renamed cond_extern to extern; removed note_thmss_accesses(_i) -- functionality covered by general naming context; diff -r e1b85512d87d -r afd2d32c7d94 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue May 31 11:53:22 2005 +0200 +++ b/src/Pure/pure_thy.ML Tue May 31 11:53:23 2005 +0200 @@ -31,7 +31,7 @@ val single_thm: string -> thm list -> thm val select_thm: thmref -> thm list -> thm list val selections: string * thm list -> (thmref * thm) list - val cond_extern_thm_sg: Sign.sg -> string -> xstring + val extern_thm_sg: Sign.sg -> string -> xstring val fact_index_of: theory -> FactIndex.T val valid_thms: theory -> thmref * thm list -> bool val thms_containing: theory -> FactIndex.spec -> (string * thm list) list @@ -45,24 +45,10 @@ val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory -> theory * thm list list - val note_thmss: - theory attribute -> ((bstring * theory attribute list) * - (thmref * theory attribute list) list) list -> theory -> - theory * (bstring * thm list) list - val note_thmss_i: - theory attribute -> ((bstring * theory attribute list) * - (thm list * theory attribute list) list) list -> theory -> - theory * (bstring * thm list) list - val note_thmss_accesses: - (string -> string list) -> - theory attribute -> ((bstring * theory attribute list) * - (thmref * theory attribute list) list) list -> theory -> - theory * (bstring * thm list) list - val note_thmss_accesses_i: - (string -> string list) -> - theory attribute -> ((bstring * theory attribute list) * - (thm list * theory attribute list) list) list -> theory -> - theory * (bstring * thm list) list + val note_thmss: theory attribute -> ((bstring * theory attribute list) * + (thmref * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list + val note_thmss_i: theory attribute -> ((bstring * theory attribute list) * + (thm list * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory @@ -119,7 +105,7 @@ Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th] | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths); - val thmss = NameSpace.cond_extern_table space theorems; + val thmss = NameSpace.extern_table space theorems; in Pretty.big_list "theorems:" (map prt_thms thmss) end; fun print sg data = Pretty.writeln (pretty sg data); @@ -129,7 +115,7 @@ val get_theorems_sg = TheoremsData.get_sg; val get_theorems = TheoremsData.get; -val cond_extern_thm_sg = NameSpace.cond_extern o #space o ! o get_theorems_sg; +val extern_thm_sg = NameSpace.extern o #space o ! o get_theorems_sg; val fact_index_of = #index o ! o get_theorems; @@ -240,7 +226,7 @@ fun valid_thms thy (thmref, ths) = (case try (transform_error (get_thms thy)) thmref of NONE => false - | SOME ths' => Library.equal_lists Thm.eq_thm (ths, ths')); + | SOME ths' => Thm.eq_thms (ths, ths')); fun thms_containing theory spec = (theory :: Theory.ancestors_of theory) @@ -271,7 +257,7 @@ fun hide_thms fully names thy = let val r as ref {space, theorems, index} = get_theorems thy; - val space' = NameSpace.hide fully (space, names); + val space' = fold (NameSpace.hide fully) names space; in r := {space = space', theorems = theorems, index = index}; thy end; @@ -299,29 +285,27 @@ fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name); fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name); -fun gen_enter_thms _ _ _ _ _ app_att thy ("", thms) = app_att (thy, thms) - | gen_enter_thms full acc sg pre_name post_name app_att thy (bname, thms) = +fun enter_thms _ _ _ app_att thy ("", thms) = app_att (thy, thms) + | enter_thms sg pre_name post_name app_att thy (bname, thms) = let - val name = full sg bname; + val name = Sign.full_name sg bname; val (thy', thms') = app_att (thy, pre_name name thms); val named_thms = post_name name thms'; val r as ref {space, theorems, index} = get_theorems_sg sg; - val space' = NameSpace.extend' acc (space, [name]); + val space' = Sign.declare_name sg name space; val theorems' = Symtab.update ((name, named_thms), theorems); val index' = FactIndex.add (K false) (name, named_thms) index; in (case Symtab.lookup (theorems, name) of NONE => () | SOME thms' => - if Library.equal_lists Thm.eq_thm (thms', named_thms) then warn_same name + if Thm.eq_thms (thms', named_thms) then warn_same name else warn_overwrite name); r := {space = space', theorems = theorems', index = index'}; (thy', named_thms) end; -fun enter_thms sg = gen_enter_thms Sign.full_name NameSpace.accesses sg; - (* add_thms(s) *) @@ -343,26 +327,21 @@ local -fun gen_note_thss enter get kind_att (thy, ((bname, more_atts), ths_atts)) = +fun gen_note_thss get kind_att (thy, ((bname, more_atts), ths_atts)) = let fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts); - val (thy', thms) = enter (Theory.sign_of thy) + val (thy', thms) = enter_thms (Theory.sign_of thy) name_thmss (name_thms false) (apsnd List.concat o foldl_map app) thy (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts); in (thy', (bname, thms)) end; -fun gen_note_thmss enter get kind_att args thy = - foldl_map (gen_note_thss enter get kind_att) (thy, args); +fun gen_note_thmss get kind_att args thy = + foldl_map (gen_note_thss get kind_att) (thy, args); in -(*if path is set, only permit unqualified names*) -val note_thmss = gen_note_thmss enter_thms get_thms; -val note_thmss_i = gen_note_thmss enter_thms (K I); - -(*always permit qualified names, clients may specify non-standard access policy*) -fun note_thmss_accesses acc = gen_note_thmss (gen_enter_thms Sign.full_name' acc) get_thms; -fun note_thmss_accesses_i acc = gen_note_thmss (gen_enter_thms Sign.full_name' acc) (K I); +val note_thmss = gen_note_thmss get_thms; +val note_thmss_i = gen_note_thmss (K I); end;