# 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 ();