renamed cond_extern to extern;
removed note_thmss_accesses(_i) -- functionality covered by general naming context;

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