diff -r 627fb639a2d9 -r e0169f13bd37 src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Mon Jul 29 16:52:04 2013 +0200
+++ b/src/Pure/PIDE/execution.ML	Mon Jul 29 18:59:58 2013 +0200
@@ -11,7 +11,6 @@
   val discontinue: unit -> unit
   val is_running: Document_ID.execution -> bool
   val running: Document_ID.execution -> Document_ID.exec -> bool
-  val finished: Document_ID.exec -> unit
   val cancel: Document_ID.exec -> unit
   val terminate: Document_ID.exec -> unit
 end;
@@ -52,12 +51,6 @@
           else execs;
       in SOME (continue, (execution_id', execs')) end);
 
-fun finished exec_id =
-  Synchronized.change state
-    (apsnd (fn execs =>
-      Inttab.delete exec_id execs handle Inttab.UNDEF bad =>
-        error ("Attempt to finish unknown execution " ^ Document_ID.print bad)));
-
 fun peek_list exec_id =
   the_list (Inttab.lookup (snd (Synchronized.value state)) exec_id);