src/Pure/Thy/thy_info.scala
changeset 59695 a03e0561bdbf
parent 59444 d57e275b2d82
child 59705 740a0ca7e09b
     1.1 --- a/src/Pure/Thy/thy_info.scala	Sat Mar 14 18:18:40 2015 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.scala	Sat Mar 14 19:51:36 2015 +0100
     1.3 @@ -106,7 +106,7 @@
     1.4            if (parent_loaded(dep.name.theory)) g
     1.5            else {
     1.6              val a = node(dep.name)
     1.7 -            val bs = dep.header.imports.map(node _)
     1.8 +            val bs = dep.header.imports.map({ case (name, _) => node(name) })
     1.9              ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
    1.10            }
    1.11        }
    1.12 @@ -136,8 +136,7 @@
    1.13          val header =
    1.14            try { resources.check_thy(session, name).cat_errors(message) }
    1.15            catch { case ERROR(msg) => cat_error(msg, message) }
    1.16 -        val imports = header.imports.map((_, Position.File(name.node)))
    1.17 -        Dep(name, header) :: require_thys(session, name :: initiators, required1, imports)
    1.18 +        Dep(name, header) :: require_thys(session, name :: initiators, required1, header.imports)
    1.19        }
    1.20        catch {
    1.21          case e: Throwable =>