tuned;
authorwenzelm
Sun Feb 26 22:41:10 2017 +0100 (2017-02-26 ago)
changeset 650549ad3f65c03f4
parent 65053 460f0fd2f77a
child 65055 12189e86c49d
tuned;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sun Feb 26 22:13:07 2017 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Feb 26 22:41:10 2017 +0100
     1.3 @@ -427,7 +427,7 @@
     1.4  
     1.5  fun local_theory restricted target f = local_theory' restricted target (K f);
     1.6  
     1.7 -fun present_local_theory target = present_transaction (fn int =>
     1.8 +fun present_local_theory target = present_transaction (fn _ =>
     1.9    (fn Theory (gthy, _) =>
    1.10          let val (finish, lthy) = Named_Target.switch target gthy;
    1.11          in Theory (finish lthy, SOME lthy) end
    1.12 @@ -561,7 +561,7 @@
    1.13  
    1.14  local
    1.15  
    1.16 -fun app int (tr as Transition {name, trans, ...}) =
    1.17 +fun app int (tr as Transition {trans, ...}) =
    1.18    setmp_thread_position tr (fn state =>
    1.19      let
    1.20        val timing_start = Timing.start ();