diff -r e2b512024eab -r ba531af91148 src/Pure/Thy/thy_load.scala --- a/src/Pure/Thy/thy_load.scala Tue Aug 07 13:21:29 2012 +0200 +++ b/src/Pure/Thy/thy_load.scala Tue Aug 07 15:01:48 2012 +0200 @@ -60,7 +60,7 @@ } } - def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Deps = + def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Header = { val name1 = header.name val imports = header.imports.map(import_name(name.dir, _)) @@ -69,10 +69,10 @@ if (name.theory != name1) error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + " for theory " + quote(name1)) - Document.Node.Deps(imports, header.keywords, uses) + Document.Node.Header(imports, header.keywords, uses) } - def check_thy(name: Document.Node.Name): Document.Node.Deps = + def check_thy(name: Document.Node.Name): Document.Node.Header = check_header(name, read_header(name)) }