src/Pure/Isar/element.ML

       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
   in proof after_qed' propss #> refine_witness #> Seq.hd end;
 
 fun proof_local cmd goal_ctxt int after_qed' propp =
   Proof.map_context (K goal_ctxt) #>
-  Proof.local_goal (K (K ())) (K I) Proof_Context.cert_propp cmd NONE
-    after_qed' (map (pair Thm.empty_binding) propp);
+  Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) cmd
+    NONE after_qed' [] (map (pair Thm.empty_binding) propp);
 
 in
 
 fun witness_proof after_qed wit_propss =
   gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits)