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;