1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 13 20:57:33 2008 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 13 20:57:33 2008 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4    val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
     1.5    val end_local_theory: transition -> transition
     1.6    val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
     1.7 -  val present_local_theory: xstring option -> (bool -> node -> unit) -> transition -> transition
     1.8 +  val present_local_theory: xstring option -> (node -> unit) -> transition -> transition
     1.9    val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
    1.10      transition -> transition
    1.11    val local_theory_to_proof: xstring option -> (local_theory -> Proof.state) ->
    1.12 @@ -73,7 +73,7 @@
    1.13    val theory_to_proof: (theory -> Proof.state) -> transition -> transition
    1.14    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
    1.15    val forget_proof: transition -> transition
    1.16 -  val present_proof: (bool -> node -> unit) -> transition -> transition
    1.17 +  val present_proof: (node -> unit) -> transition -> transition
    1.18    val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition
    1.19    val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
    1.20    val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
    1.21 @@ -503,7 +503,7 @@
    1.22            val finish = loc_finish loc gthy;
    1.23            val lthy' = f (loc_begin loc gthy);
    1.24          in Theory (finish lthy', SOME lthy') end
    1.25 -    | _ => raise UNDEF) #> tap (g int));
    1.26 +    | _ => raise UNDEF) #> tap g);
    1.27  
    1.28  in
    1.29  
    1.30 @@ -564,10 +564,10 @@
    1.31      | SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
    1.32      | _ => raise UNDEF));
    1.33  
    1.34 -fun present_proof f = transaction (fn int =>
    1.35 +fun present_proof f = transaction (fn _ =>
    1.36    (fn Proof (prf, x) => Proof (ProofNode.apply I prf, x)
    1.37      | skip as SkipProof _ => skip
    1.38 -    | _ => raise UNDEF) #> tap (f int));
    1.39 +    | _ => raise UNDEF) #> tap f);
    1.40  
    1.41  fun proofs' f = transaction (fn int =>
    1.42    (fn Proof (prf, x) => Proof (ProofNode.applys (f int) prf, x)