--- 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;