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