--- 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;