src/Pure/Thy/thy_syntax.scala

 
         case (name, Document.Node.Header(header)) =>
           val node = nodes(name)
           val update_header =
             (node.header, header) match {
-              case (Exn.Res(thy_header0), Exn.Res(thy_header)) => thy_header0 != thy_header
+              case (Exn.Res(deps0), Exn.Res(deps)) => deps != deps
               case _ => true
             }
           if (update_header) {
             doc_edits += (name -> Document.Node.Header(header))
             nodes += (name -> node.update_header(header))