src/Pure/PIDE/document.ML

--- a/src/Pure/PIDE/document.ML	Tue Nov 09 21:13:06 2010 +0100
+++ b/src/Pure/PIDE/document.ML	Tue Nov 09 21:44:19 2010 +0100
@@ -34,16 +34,7 @@
 type exec_id = id;
 
 val no_id = 0;
-
-local
-  val id_count = Synchronized.var "id" 0;
-in
-  fun new_id () =
-    Synchronized.change_result id_count
-      (fn i =>
-        let val i' = i + 1
-        in (i', i') end);
-end;
+val new_id = Synchronized.counter ();
 
 val parse_id = Markup.parse_int;
 val print_id = Markup.print_int;