changeset 63510 | 0fc8be2f8176 |
parent 63451 | c4c587aedee8 |
child 63513 | 9f8d06f23c09 |
--- a/src/Pure/Pure.thy Fri Jul 15 22:23:36 2016 +0200 +++ b/src/Pure/Pure.thy Fri Jul 15 23:46:28 2016 +0200 @@ -902,7 +902,7 @@ val _ = Outer_Syntax.command @{command_keyword proof} "backward proof step" (Scan.option Method.parse >> (fn m => - (Option.map Method.report m; Toplevel.proofs (Proof.proof m)))); + (Option.map Method.report m; Toplevel.proof (Proof.proof m #> Seq.the_result "")))); in end\<close>