diff -r ecb51b457064 -r 1de22a7b2a82 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Aug 13 15:59:26 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Aug 13 16:04:28 2011 +0200
@@ -53,9 +53,9 @@
     case class Edits[A](edits: List[A]) extends Edit[A]
     case class Header[A](header: Node_Header) extends Edit[A]
 
-    def norm_header[A](f: Path => String, header: Node_Header): Header[A] =
+    def norm_header[A](f: String => String, header: Node_Header): Header[A] =
       header match {
-        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(name => f(Path.explode(name))) })
+        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f) })
         case exn => Header[A](exn)
       }