src/Pure/Pure.thy
changeset 63513 9f8d06f23c09
parent 63510 0fc8be2f8176
child 63579 73939a9b70a3
     1.1 --- a/src/Pure/Pure.thy	Sat Jul 16 00:11:03 2016 +0200
     1.2 +++ b/src/Pure/Pure.thy	Sat Jul 16 00:38:33 2016 +0200
     1.3 @@ -902,7 +902,14 @@
     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.proof (Proof.proof m #> Seq.the_result ""))));
     1.8 +      (Option.map Method.report m;
     1.9 +       Toplevel.proof (fn state =>
    1.10 +         let
    1.11 +          val state' = state |> Proof.proof m |> Seq.the_result "";
    1.12 +          val _ =
    1.13 +            Output.information
    1.14 +              (Proof_Context.print_cases_proof (Proof.context_of state) (Proof.context_of state'));
    1.15 +        in state' end))))
    1.16  
    1.17  in end\<close>
    1.18