# HG changeset patch
# User wenzelm
# Date 1118311493 -7200
# Node ID d7f9978e5752c30e731802b5bf8a24d8d9ec4ff0
# Parent  561b9f8be72e568e5e22ce1960ecc0ec1b2adc7c
axioms: NameSpace.table;

diff -r 561b9f8be72e -r d7f9978e5752 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Jun 09 12:03:38 2005 +0200
+++ b/src/Pure/thm.ML	Thu Jun 09 12:04:53 2005 +0200
@@ -483,7 +483,7 @@
   let
     fun get_ax [] = NONE
       | get_ax (thy :: thys) =
-          let val {sign, axioms, ...} = Theory.rep_theory thy in
+          let val {sign, axioms = (_, axioms), ...} = Theory.rep_theory thy in
             (case Symtab.lookup (axioms, name) of
               SOME t =>
                 SOME (fix_shyps [] []
@@ -503,7 +503,8 @@
     | NONE => raise THEORY ("No axiom " ^ quote name, [theory]))
   end;
 
-fun get_axiom thy = get_axiom_i thy o Sign.intern (Theory.sign_of thy) Theory.axiomK;
+fun get_axiom thy =
+  get_axiom_i thy o NameSpace.intern (#1 (#axioms (Theory.rep_theory thy)));
 
 fun def_name name = name ^ "_def";
 fun get_def thy = get_axiom thy o def_name;
@@ -512,7 +513,7 @@
 (*return additional axioms of this theory node*)
 fun axioms_of thy =
   map (fn (s, _) => (s, get_axiom thy s))
-    (Symtab.dest (#axioms (Theory.rep_theory thy)));
+    (Symtab.dest (#2 (#axioms (Theory.rep_theory thy))));
 
 
 (* name and tags -- make proof objects more readable *)
@@ -1443,7 +1444,7 @@
 
 fun invoke_oracle_i thy name =
   let
-    val {sign = sg, oracles, ...} = Theory.rep_theory thy;
+    val {sign = sg, oracles = (_, oracles), ...} = Theory.rep_theory thy;
     val oracle =
       (case Symtab.lookup (oracles, name) of
         NONE => raise THM ("Unknown oracle: " ^ name, 0, [])
@@ -1470,7 +1471,7 @@
   end;
 
 fun invoke_oracle thy =
-  invoke_oracle_i thy o Sign.intern (Theory.sign_of thy) Theory.oracleK;
+  invoke_oracle_i thy o NameSpace.intern (#1 (#oracles (Theory.rep_theory thy)));
 
 
 end;