Fix two variants of Node::substitute().
authorMorgan Deters <mdeters@cs.nyu.edu>
Fri, 21 Feb 2014 19:45:52 +0000 (14:45 -0500)
committerMorgan Deters <mdeters@cs.nyu.edu>
Fri, 21 Feb 2014 20:06:14 +0000 (15:06 -0500)
commitb712a12978ea0c1f0f57bb72e28dc1286dc8ac69
tree1ffd38eebe3fdd1259857b55d8badf7044afa588
parentcca221de7d29e86fd770af3aca0efc0d877dff26
Fix two variants of Node::substitute().

Node::substitute() is overloaded.  One version was properly substituting
operators (e.g. the "f" in f(x) could be substituted).  The others were
ignoring anything in function position.  Fixed.  Thanks to Wei Wang for
pointing this out.
src/expr/node.h