# HG changeset patch
# User wenzelm
# Date 1345548574 -7200
# Node ID c82720f054c340ed8e3cc73a08b222e34bf1c266
# Parent  4accee106f0f7e71cec33b8f1915842bd2d50c1d
tuned signature;

diff -r 4accee106f0f -r c82720f054c3 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Tue Aug 21 12:15:25 2012 +0200
+++ b/src/Pure/Thy/thy_info.scala	Tue Aug 21 13:29:34 2012 +0200
@@ -25,7 +25,13 @@
   /* dependencies */
 
   type Dep = (Document.Node.Name, Document.Node.Header)
-  private type Required = (List[Dep], Set[Document.Node.Name])
+  private sealed case class Required(
+    deps: List[Dep] = Nil,
+    seen: Set[Document.Node.Name] = Set.empty)
+  {
+    def :: (dep: Dep): Required = copy(deps = dep :: deps)
+    def + (name: Document.Node.Name): Required = copy(seen = seen + name)
+  }
 
   private def require_thys(initiators: List[Document.Node.Name],
       required: Required, names: List[Document.Node.Name]): Required =
@@ -34,9 +40,8 @@
   private def require_thy(initiators: List[Document.Node.Name],
       required: Required, name: Document.Node.Name): Required =
   {
-    val (deps, seen) = required
-    if (seen(name)) required
-    else if (thy_load.loaded_theories(name.theory)) (deps, seen + name)
+    if (required.seen(name)) required
+    else if (thy_load.loaded_theories(name.theory)) required + name
     else {
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
@@ -47,17 +52,15 @@
               cat_error(msg, "The error(s) above occurred while examining theory " +
                 quote(name.theory) + required_by(initiators))
           }
-        val (deps1, seen1) =
-          require_thys(name :: initiators, (deps, seen + name), header.imports)
-        ((name, header) :: deps1, seen1)
+        (name, header) :: require_thys(name :: initiators, required + name, header.imports)
       }
       catch {
         case e: Throwable =>
-          ((name, Document.Node.bad_header(Exn.message(e))) :: deps, seen + name)
+          (name, Document.Node.bad_header(Exn.message(e))) :: (required + name)
       }
     }
   }
 
   def dependencies(names: List[Document.Node.Name]): List[Dep] =
-    require_thys(Nil, (Nil, Set.empty), names)._1.reverse
+    require_thys(Nil, Required(), names).deps.reverse
 }