diff -r 6fab87db556c -r 58c4f3e1870f src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Thu Jan 29 13:50:53 2015 +0100
+++ b/src/Pure/PIDE/execution.ML	Thu Jan 29 13:58:02 2015 +0100
@@ -14,7 +14,6 @@
   val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool
   val peek: Document_ID.exec -> Future.group list
   val cancel: Document_ID.exec -> unit
-  val terminate: Document_ID.exec -> unit
   type params = {name: string, pos: Position.T, pri: int}
   val fork: params -> (unit -> 'a) -> 'a future
   val print: params -> (unit -> unit) -> unit
@@ -76,7 +75,6 @@
   | NONE => []);
 
 fun cancel exec_id = List.app Future.cancel_group (peek exec_id);
-fun terminate exec_id = List.app Future.terminate (peek exec_id);
 
 
 (* fork *)