src/Pure/Isar/toplevel.ML

   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
   val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
   val end_local_theory: transition -> transition
   val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
-  val present_local_theory: xstring option -> (bool -> node -> unit) -> transition -> transition
+  val present_local_theory: xstring option -> (node -> unit) -> transition -> transition
   val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
     transition -> transition
   val local_theory_to_proof: xstring option -> (local_theory -> Proof.state) ->
     transition -> transition
   val theory_to_proof: (theory -> Proof.state) -> transition -> transition
   val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
   val forget_proof: transition -> transition
-  val present_proof: (bool -> node -> unit) -> transition -> transition
+  val present_proof: (node -> unit) -> transition -> transition
   val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition
   val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
   val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
   val proof: (Proof.state -> Proof.state) -> transition -> transition
   val actual_proof: (ProofNode.T -> ProofNode.T) -> transition -> transition

   (fn Theory (gthy, _) =>
         let
           val finish = loc_finish loc gthy;
           val lthy' = f (loc_begin loc gthy);
         in Theory (finish lthy', SOME lthy') end
-    | _ => raise UNDEF) #> tap (g int));
+    | _ => raise UNDEF) #> tap g);
 
 in
 
 fun local_theory loc f = local_theory_presentation loc f (K I);
 fun present_local_theory loc g = local_theory_presentation loc I g;

 val forget_proof = transaction (fn _ =>
   (fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
     | SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
     | _ => raise UNDEF));
 
-fun present_proof f = transaction (fn int =>
+fun present_proof f = transaction (fn _ =>
   (fn Proof (prf, x) => Proof (ProofNode.apply I prf, x)
     | skip as SkipProof _ => skip
-    | _ => raise UNDEF) #> tap (f int));
+    | _ => raise UNDEF) #> tap f);
 
 fun proofs' f = transaction (fn int =>
   (fn Proof (prf, x) => Proof (ProofNode.applys (f int) prf, x)
     | skip as SkipProof _ => skip
     | _ => raise UNDEF));