src/Pure/Isar/element.ML

--- a/src/Pure/Isar/element.ML	Tue Jun 09 15:28:06 2015 +0200
+++ b/src/Pure/Isar/element.ML	Tue Jun 09 16:07:11 2015 +0200
@@ -280,8 +280,8 @@
 
 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