src/Pure/Thy/thy_header.scala
changeset 44163 32e0c150c010
parent 44160 8848867501fb
child 44185 05641edb5d30
     1.1 --- a/src/Pure/Thy/thy_header.scala	Fri Aug 12 20:32:25 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Aug 12 22:10:49 2011 +0200
     1.3 @@ -110,5 +110,8 @@
     1.4  {
     1.5    def map(f: String => String): Thy_Header =
     1.6      Thy_Header(f(name), imports.map(f), uses.map(f))
     1.7 +
     1.8 +  def norm_deps(f: String => String): Thy_Header =
     1.9 +    copy(imports = imports.map(name => f(name) + ".thy"), uses = uses.map(f))
    1.10  }
    1.11