summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Pure/Isar/toplevel.ML

changeset 49863 | b5fb6e7f8d81 |

parent 49062 | 7e31dfd99ce7 |

child 50201 | c26369c9eda6 |

--- a/src/Pure/Isar/toplevel.ML Tue Oct 16 15:02:49 2012 +0200 +++ b/src/Pure/Isar/toplevel.ML Tue Oct 16 15:14:12 2012 +0200 @@ -74,9 +74,9 @@ val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition val forget_proof: transition -> transition val present_proof: (state -> unit) -> transition -> transition - val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition + val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition - val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition + val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition val proof: (Proof.state -> Proof.state) -> transition -> transition val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition val skip_proof: (int -> int) -> transition -> transition @@ -556,7 +556,7 @@ | skip as SkipProof _ => skip | _ => raise UNDEF)); -fun proof' f = proofs' (Seq.single oo f); +fun proof' f = proofs' ((Seq.single o Seq.Result) oo f); val proofs = proofs' o K; val proof = proof' o K;