# HG changeset patch
# User wenzelm
# Date 1126797426 -7200
# Node ID cd5d8b444d6ed072cd7a31b2c862f8d2b41a8330
# Parent  c56f4809fc6d0fc154045eb34e3ac5fb6ee188b4
TableFun/Symtab: curried lookup and update;
add_defs etc.: use Thm.get_axiom_i, which is independent from naming;

diff -r c56f4809fc6d -r cd5d8b444d6e src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Sep 15 17:17:05 2005 +0200
+++ b/src/Pure/pure_thy.ML	Thu Sep 15 17:17:06 2005 +0200
@@ -211,7 +211,7 @@
   in
     fn name =>
       Option.map (map (Thm.transfer (Theory.deref thy_ref)))     (*dynamic identity*)
-      (Symtab.curried_lookup thms (NameSpace.intern space name)) (*static content*)
+      (Symtab.lookup thms (NameSpace.intern space name)) (*static content*)
   end;
 
 fun get_thms_closure thy =
@@ -311,10 +311,10 @@
         val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms));
         val r as ref {theorems = (space, theorems), index} = get_theorems_ref thy';
         val space' = Sign.declare_name thy' name space;
-        val theorems' = Symtab.curried_update (name, thms') theorems;
+        val theorems' = Symtab.update (name, thms') theorems;
         val index' = FactIndex.add (K false) (name, thms') index;
       in
-        (case Symtab.curried_lookup theorems name of
+        (case Symtab.lookup theorems name of
           NONE => ()
         | SOME thms'' =>
             if Thm.eq_thms (thms', thms'') then warn_same name
@@ -415,8 +415,8 @@
 (* store axioms as theorems *)
 
 local
-  fun get_axs thy named_axs =
-    map (forall_elim_vars 0 o Thm.get_axiom thy o fst) named_axs;
+  fun get_ax thy (name, _) = Thm.get_axiom_i thy (Sign.full_name thy name);
+  fun get_axs thy named_axs = map (forall_elim_vars 0 o get_ax thy) named_axs;
 
   fun add_single add (thy, ((name, ax), atts)) =
     let