Fix bug #456
This reduces the time spent in Term.t_compare
and Term.t_hash
. On #456 (closed), time is divided by four.
A further 30% improvement can be obtained by disabling the computation of unknown identifiers in Decl.d_node
for goal declarations, but the change is deemed too unsafe by @paskevyc and I. (Transformations would have to be careful that goals contain only known identifiers.)