# HG changeset patch
# User wenzelm
# Date 1488145270 -3600
# Node ID 9ad3f65c03f4e5025bd1003d617e00f00cefe179
# Parent  460f0fd2f77a5e3acddd7640ff4931ae7b1c53e8
tuned;

diff -r 460f0fd2f77a -r 9ad3f65c03f4 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Feb 26 22:13:07 2017 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sun Feb 26 22:41:10 2017 +0100
@@ -427,7 +427,7 @@
 
 fun local_theory restricted target f = local_theory' restricted target (K f);
 
-fun present_local_theory target = present_transaction (fn int =>
+fun present_local_theory target = present_transaction (fn _ =>
   (fn Theory (gthy, _) =>
         let val (finish, lthy) = Named_Target.switch target gthy;
         in Theory (finish lthy, SOME lthy) end
@@ -561,7 +561,7 @@
 
 local
 
-fun app int (tr as Transition {name, trans, ...}) =
+fun app int (tr as Transition {trans, ...}) =
   setmp_thread_position tr (fn state =>
     let
       val timing_start = Timing.start ();