diff -r 9a8f4fdac3cf -r 960202346d0c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jun 26 09:58:39 2013 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jun 26 11:54:45 2013 +0200
@@ -1133,8 +1133,7 @@
 
     val prop' = Logic.protect prop;
     val statement' = (kind, [[], [prop']], prop');
-    val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)
-      (Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
+    val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal) (Goal.protect (Thm.nprems_of goal) goal);
     val after_qed' = (fn [[th]] => map_context (set_result th), fn [[th]] => set_result th);
 
     val result_ctxt =