src/Pure/Thy/thy_header.scala
changeset 44578 ca3844a3dcf7
parent 44225 a8f921e6484f
child 46676 b4bc54d4624b
     1.1 --- a/src/Pure/Thy/thy_header.scala	Tue Aug 30 11:43:47 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Aug 30 12:01:07 2011 +0200
     1.3 @@ -119,6 +119,8 @@
     1.4      Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
     1.5  
     1.6    def norm_deps(f: String => String, g: String => String): Thy_Header =
     1.7 -    copy(imports = imports.map(name => f(name)), uses = uses.map(p => (g(p._1), p._2)))
     1.8 +    copy(imports = imports.map(name => f(name)))
     1.9 +    // FIXME
    1.10 +    // copy(imports = imports.map(name => f(name)), uses = uses.map(p => (g(p._1), p._2)))
    1.11  }
    1.12