1.1 --- a/src/Pure/library.scala	Mon Feb 27 23:30:38 2012 +0100
     1.2 +++ b/src/Pure/library.scala	Mon Feb 27 23:35:11 2012 +0100
     1.3 @@ -128,26 +128,6 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* graph traversal */
     1.8 -
     1.9 -  def topological_order[A](next: A => Iterable[A], starts: Iterable[A]): List[A] =
    1.10 -  {
    1.11 -    type Reached = (List[A], Set[A])
    1.12 -    def reach(reached: Reached, x: A): Reached =
    1.13 -    {
    1.14 -      val (rs, r_set) = reached
    1.15 -      if (r_set(x)) reached
    1.16 -      else {
    1.17 -        val (rs1, r_set1) = reachs((rs, r_set + x), next(x))
    1.18 -        (x :: rs1, r_set1)
    1.19 -      }
    1.20 -    }
    1.21 -    def reachs(reached: Reached, xs: Iterable[A]): Reached = (reached /: xs)(reach)
    1.22 -
    1.23 -    reachs((Nil, Set.empty), starts)._1.reverse
    1.24 -  }
    1.25 -
    1.26 -
    1.27    /* simple dialogs */
    1.28  
    1.29    private def simple_dialog(kind: Int, default_title: String)