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