changeset 29383 | 223f18cfbb32 |
parent 29362 | f9ded2d789b9 |
child 29394 | 4638ab6c878f |
--- a/src/Pure/Isar/expression.ML Wed Jan 07 12:10:22 2009 +0100 +++ b/src/Pure/Isar/expression.ML Wed Jan 07 16:22:10 2009 +0100 @@ -887,7 +887,7 @@ end; fun after_qed results = - Proof.map_context (fold store_reg (regs ~~ prep_result propss results)) #> Seq.single; + Proof.map_context (fold store_reg (regs ~~ prep_result propss results)); in state |> Proof.map_context (K goal_ctxt) |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i