singleton result for 'proof' command (without backtracking), e.g. relevant for well-defined output;
authorwenzelm
Fri Jul 15 23:46:28 2016 +0200 (2016-07-15)
changeset 635100fc8be2f8176
parent 63509 3b9ab054a356
child 63511 1c2c045decb3
singleton result for 'proof' command (without backtracking), e.g. relevant for well-defined output;
src/Pure/Pure.thy
     1.1 --- a/src/Pure/Pure.thy	Fri Jul 15 22:23:36 2016 +0200
     1.2 +++ b/src/Pure/Pure.thy	Fri Jul 15 23:46:28 2016 +0200
     1.3 @@ -902,7 +902,7 @@
     1.4  val _ =
     1.5    Outer_Syntax.command @{command_keyword proof} "backward proof step"
     1.6      (Scan.option Method.parse >> (fn m =>
     1.7 -      (Option.map Method.report m; Toplevel.proofs (Proof.proof m))));
     1.8 +      (Option.map Method.report m; Toplevel.proof (Proof.proof m #> Seq.the_result ""))));
     1.9  
    1.10  in end\<close>
    1.11