# HG changeset patch
# User wenzelm
# Date 1330612964 -3600
# Node ID 042c546d2baca3bc3141197e46a8a76d0c2092ad
# Parent  8f3ae4d04a2d7054a125e97c75d372609a250d6c
proper update_header;

diff -r 8f3ae4d04a2d -r 042c546d2bac src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Mar 01 15:16:20 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Mar 01 15:42:44 2012 +0100
@@ -258,7 +258,7 @@
           val node = nodes(name)
           val update_header =
             (node.header, header) match {
-              case (Exn.Res(deps0), Exn.Res(deps)) => deps != deps
+              case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps
               case _ => true
             }
           if (update_header) {