src/Pure/Isar/toplevel.ML
changeset 49863 b5fb6e7f8d81
parent 49062 7e31dfd99ce7
child 50201 c26369c9eda6
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Oct 16 15:02:49 2012 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Oct 16 15:14:12 2012 +0200
     1.3 @@ -74,9 +74,9 @@
     1.4    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
     1.5    val forget_proof: transition -> transition
     1.6    val present_proof: (state -> unit) -> transition -> transition
     1.7 -  val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition
     1.8 +  val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
     1.9    val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
    1.10 -  val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
    1.11 +  val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
    1.12    val proof: (Proof.state -> Proof.state) -> transition -> transition
    1.13    val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
    1.14    val skip_proof: (int -> int) -> transition -> transition
    1.15 @@ -556,7 +556,7 @@
    1.16      | skip as SkipProof _ => skip
    1.17      | _ => raise UNDEF));
    1.18  
    1.19 -fun proof' f = proofs' (Seq.single oo f);
    1.20 +fun proof' f = proofs' ((Seq.single o Seq.Result) oo f);
    1.21  val proofs = proofs' o K;
    1.22  val proof = proof' o K;
    1.23