--- a/src/Pure/thm.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/thm.ML Sun Mar 18 13:04:22 2012 +0100
@@ -1772,9 +1772,7 @@
fun add_oracle (b, oracle) thy =
let
- val naming = Sign.naming_of thy;
- val (name, tab') =
- Name_Space.define (Proof_Context.init_global thy) true naming (b, ()) (Oracles.get thy);
+ val (name, tab') = Name_Space.define (Context.Theory thy) true (b, ()) (Oracles.get thy);
val thy' = Oracles.put tab' thy;
in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;