src/Pure/Isar/toplevel.ML
changeset 59000 ed09ae4ea2d8
parent 58923 cb9b69cca999
child 59032 f36496364ce1
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Nov 13 17:28:11 2014 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Nov 13 23:45:15 2014 +0100
     1.3 @@ -65,7 +65,6 @@
     1.4    val theory_to_proof: (theory -> Proof.state) -> transition -> transition
     1.5    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
     1.6    val forget_proof: bool -> transition -> transition
     1.7 -  val present_proof: (state -> unit) -> 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.result Seq.seq) -> transition -> transition
    1.11 @@ -498,11 +497,6 @@
    1.12      | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
    1.13      | _ => raise UNDEF));
    1.14  
    1.15 -val present_proof = present_transaction (fn _ =>
    1.16 -  (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
    1.17 -    | skip as Skipped_Proof _ => skip
    1.18 -    | _ => raise UNDEF));
    1.19 -
    1.20  fun proofs' f = transaction (fn int =>
    1.21    (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
    1.22      | skip as Skipped_Proof _ => skip