src/Pure/Isar/isar_thy.ML

   #> tap (present_theorems kind);
 
 fun apply_theorems args = apfst (maps snd) o theorems "" [(("", []), args)];
 fun apply_theorems_i args = apfst (maps snd) o theorems_i "" [(("", []), args)];
 
+(* FIXME local_theory *)
 fun smart_theorems kind NONE args thy = thy
       |> theorems kind args
       |> tap (present_theorems kind)
       |> (fn (_, thy) => `ProofContext.init thy)
   | smart_theorems kind (SOME loc) args thy = thy
       |> Locale.note_thmss kind loc args
+      ||> (fn ctxt' => (ctxt', ProofContext.theory_of ctxt'))
       |> tap (fn ((_, res), (_, thy')) => present_theorems kind (res, thy'))
       |> #2;
 
 fun declare_theorems opt_loc args =
   smart_theorems "" opt_loc [(("", []), args)];

 
 
 (* global endings *)
 
 fun global_ending ending = Toplevel.proof_to_theory_context (fn int => fn state =>
-  if can (Proof.assert_bottom true) state then ending int state
+  if can (Proof.assert_bottom true) state then
+    ending int state |> (fn ctxt' => (ctxt', ProofContext.theory_of ctxt'))
   else raise Toplevel.UNDEF);
 
 fun global_qed m = global_ending (K (Proof.global_qed (m, true)));
 val global_terminal_proof = global_ending o K o Proof.global_terminal_proof;
 val global_default_proof = global_ending (K Proof.global_default_proof);