# HG changeset patch
# User wenzelm
# Date 1468619188 -7200
# Node ID 0fc8be2f8176d8588ef9d9a32f52fdbb549e4564
# Parent  3b9ab054a3563d7d1f1252b297594d4dd5a1b39d
singleton result for 'proof' command (without backtracking), e.g. relevant for well-defined output;

diff -r 3b9ab054a356 -r 0fc8be2f8176 src/Pure/Pure.thy
--- 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>