# HG changeset patch
# User wenzelm
# Date 1218653853 -7200
# Node ID c1bc9f4df521b47e170680e7bdbc8a4f9f0e9e89
# Parent  d385b67f84395dfb08f84617571e04c8c8be17ee
simplified present_local_theory/proof;

diff -r d385b67f8439 -r c1bc9f4df521 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Aug 13 20:57:33 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Aug 13 20:57:33 2008 +0200
@@ -65,7 +65,7 @@
   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) ->
@@ -73,7 +73,7 @@
   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
@@ -503,7 +503,7 @@
           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
 
@@ -564,10 +564,10 @@
     | 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)