proper update_header;
authorwenzelm
Thu, 01 Mar 2012 15:42:44 +0100
changeset 46749 042c546d2bac
parent 46748 8f3ae4d04a2d
child 46750 69efe9b2994c
proper update_header;
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) {