# HG changeset patch
# User wenzelm
# Date 1222810298 -7200
# Node ID 0790f66a931a0e2142503d7407c0a9c33c4fc322
# Parent  4faf705a177df46ff737cd685e28a29f861a9b8e
promise_proof: proper statement with empty vars;

diff -r 4faf705a177d -r 0790f66a931a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Sep 30 23:31:36 2008 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Sep 30 23:31:38 2008 +0200
@@ -997,7 +997,7 @@
     val {statement as (kind, propss, cprop), messages, using, goal, before_qed, after_qed} = goal;
     val prop = Thm.term_of cprop;
 
-    val statement' = (kind, [[prop]], cprop);
+    val statement' = (kind, [[], [prop]], cprop);
     fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
     val this_name = ProofContext.full_name (ProofContext.reset_naming goal_ctxt) AutoBind.thisN;