diff r 6237574c705b r ed09ae4ea2d8 src/Pure/Isar/toplevel.ML
 a/src/Pure/Isar/toplevel.ML Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML Thu Nov 13 23:45:15 2014 +0100
@@ 65,7 +65,6 @@
val theory_to_proof: (theory > Proof.state) > transition > transition
val end_proof: (bool > Proof.state > Proof.context) > transition > transition
val forget_proof: bool > transition > transition
 val present_proof: (state > unit) > 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.result Seq.seq) > transition > transition
@@ 498,11 +497,6 @@
 Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
 _ => raise UNDEF));
val present_proof = present_transaction (fn _ =>
 (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
  skip as Skipped_Proof _ => skip
  _ => raise UNDEF));

fun proofs' f = transaction (fn int =>
(fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
 skip as Skipped_Proof _ => skip