--- 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\