# HG changeset patch
# User wenzelm
# Date 1112858883 -7200
# Node ID 32aea1e31eb8c8dea573d613357d3286bb922194
# Parent  8df681866dc96009ff4e42de86ab9397129a53f3
added get_axiom_i, invoke_oracle_i;

diff -r 8df681866dc9 -r 32aea1e31eb8 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Apr 07 09:27:50 2005 +0200
+++ b/src/Pure/thm.ML	Thu Apr 07 09:28:03 2005 +0200
@@ -61,6 +61,7 @@
   val cprop_of          : thm -> cterm
   val extra_shyps       : thm -> sort list
   val strip_shyps       : thm -> thm
+  val get_axiom_i       : theory -> string -> thm
   val get_axiom         : theory -> xstring -> thm
   val def_name		: string -> string
   val get_def           : theory -> xstring -> thm
@@ -104,6 +105,7 @@
     int -> thm -> thm Seq.seq
   val biresolution      : bool -> (bool * thm) list ->
     int -> thm -> thm Seq.seq
+  val invoke_oracle_i   : theory -> string -> Sign.sg * Object.T -> thm
   val invoke_oracle     : theory -> xstring -> Sign.sg * Object.T -> thm
 end;
 
@@ -475,10 +477,8 @@
 (** Axioms **)
 
 (*look up the named axiom in the theory*)
-fun get_axiom theory raw_name =
+fun get_axiom_i theory name =
   let
-    val name = Sign.intern (Theory.sign_of theory) Theory.axiomK raw_name;
-
     fun get_ax [] = NONE
       | get_ax (thy :: thys) =
           let val {sign, axioms, ...} = Theory.rep_theory thy in
@@ -501,6 +501,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 def_name name = name ^ "_def";
 fun get_def thy = get_axiom thy o def_name;
 
@@ -1454,10 +1456,9 @@
 
 (*** Oracles ***)
 
-fun invoke_oracle thy raw_name =
+fun invoke_oracle_i thy name =
   let
     val {sign = sg, oracles, ...} = Theory.rep_theory thy;
-    val name = Sign.intern sg Theory.oracleK raw_name;
     val oracle =
       (case Symtab.lookup (oracles, name) of
         NONE => raise THM ("Unknown oracle: " ^ name, 0, [])
@@ -1483,6 +1484,9 @@
       end
   end;
 
+fun invoke_oracle thy =
+  invoke_oracle_i thy o Sign.intern (Theory.sign_of thy) Theory.oracleK;
+
 
 end;