diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/thm.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -147,7 +147,7 @@
   val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
   val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
   val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
-  val extern_oracles: theory -> xstring list
+  val extern_oracles: Proof.context -> xstring list
   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
 end;
 
@@ -1734,7 +1734,8 @@
   fun merge data : T = Name_Space.merge_tables data;
 );
 
-val extern_oracles = map #1 o Name_Space.extern_table o Oracles.get;
+fun extern_oracles ctxt =
+  map #1 (Name_Space.extern_table ctxt (Oracles.get (ProofContext.theory_of ctxt)));
 
 fun add_oracle (b, oracle) thy =
   let