diff -r 8cf877aca29a -r 4ced3c6ad807 src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Fri Jul 17 17:17:39 2015 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML	Fri Jul 17 21:00:41 2015 +0200
@@ -395,17 +395,17 @@
 
 val _ =
   Isabelle_Process.protocol_command "Simplifier_Trace.reply"
-    (fn [s, r] =>
+    (fn [serial_string, reply] =>
       let
-        val serial = Markup.parse_int s
-        fun lookup_delete tab =
-          (Inttab.lookup tab serial, Inttab.delete_safe serial tab)
-        fun apply_result (SOME promise) = Future.fulfill promise r
-          | apply_result NONE = () (* FIXME handle protocol failure, just like in active.ML? *)
+        val serial = Markup.parse_int serial_string
+        val result =
+          Synchronized.change_result futures
+            (fn tab => (Inttab.lookup tab serial, Inttab.delete_safe serial tab))
       in
-        (Synchronized.change_result futures lookup_delete |> apply_result)
-          handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn
-      end)
+        (case result of
+          SOME promise => Future.fulfill promise reply
+        | NONE => ()) (* FIXME handle protocol failure, just like in active.ML (!?) *)
+      end handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn)