singleton result for 'proof' command (without backtracking), e.g. relevant for well-defined output;
--- 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>