src/Pure/Isar/element.ML

--- a/src/Pure/Isar/element.ML	Wed Jun 10 11:52:54 2015 +0200
+++ b/src/Pure/Isar/element.ML	Wed Jun 10 14:46:31 2015 +0200
@@ -281,7 +281,7 @@
 fun proof_local cmd goal_ctxt int after_qed' propp =
   Proof.map_context (K goal_ctxt) #>
   Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) cmd
-    NONE after_qed' [] (map (pair Thm.empty_binding) propp);
+    NONE after_qed' [] [] (map (pair Thm.empty_binding) propp);
 
 in