# HG changeset patch
# User wenzelm
# Date 1398449259 -7200
# Node ID 6dc97c5aaf5e8a021e7fa84469253518fde0e843
# Parent  ba1ac087b3a771b1cf35959ae36511b299baef54
unused;

diff -r ba1ac087b3a7 -r 6dc97c5aaf5e src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Fri Apr 25 17:54:54 2014 +0200
+++ b/src/Pure/Thy/thy_info.scala	Fri Apr 25 20:07:39 2014 +0200
@@ -7,9 +7,6 @@
 package isabelle
 
 
-import java.util.concurrent.{Future => JFuture}
-
-
 class Thy_Info(resources: Resources)
 {
   /* messages */
diff -r ba1ac087b3a7 -r 6dc97c5aaf5e src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Apr 25 17:54:54 2014 +0200
+++ b/src/Pure/library.scala	Fri Apr 25 20:07:39 2014 +0200
@@ -159,18 +159,6 @@
   def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
   def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
   def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
-
-
-  /* Java futures */
-
-  def future_value[A](x: A) = new JFuture[A]
-  {
-    def cancel(may_interrupt: Boolean): Boolean = false
-    def isCancelled(): Boolean = false
-    def isDone(): Boolean = true
-    def get(): A = x
-    def get(timeout: Long, time_unit: TimeUnit): A = x
-  }
 }