--- a/src/Pure/Isar/obtain.ML Wed Jun 26 09:58:39 2013 +0200
+++ b/src/Pure/Isar/obtain.ML Wed Jun 26 11:54:45 2013 +0200
@@ -301,7 +301,7 @@
fun print_result ctxt' (k, [(s, [_, th])]) =
Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]);
val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #>
- (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
+ (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
fun after_qed [[_, res]] =
Proof.end_block #> guess_context (check_result ctxt thesis res);
in