diff -r a6cad32a27b0 -r 6561665c5cb1 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 14:41:09 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 14:41:10 2008 +0100
@@ -201,7 +201,7 @@
     \  val name = " ^ quote name ^ ";\n\
     \  exception Arg of T;\n\
     \  val _ = Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\
-    \  val thy = ML_Context.the_context ();\n\
+    \  val thy = ML_Context.the_global_context ();\n\
     \  val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
     \in\n\
     \  fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\