# HG changeset patch
# User wenzelm
# Date 1373280459 -7200
# Node ID 9e6b59cd5560a7e36073a51726ad2cc5d8e052d8
# Parent  ddaf277e0d8c25dccc9d2640bd5186e44930f8ec
tuned;

diff -r ddaf277e0d8c -r 9e6b59cd5560 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Jul 08 12:07:06 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Jul 08 12:47:39 2013 +0200
@@ -75,12 +75,12 @@
     NONE => ()
   | SOME id =>
       let
-        val (n, ok) =
+        val ok =
           Synchronized.change_result tracing_messages (fn tab =>
             let
               val n = the_default 0 (Inttab.lookup tab id) + 1;
               val ok = n <= Options.default_int "editor_tracing_messages";
-            in ((n, ok), Inttab.update (id, n) tab) end);
+            in (ok, Inttab.update (id, n) tab) end);
       in
         if ok then ()
         else