pass thy as explicit argument (the old ref was not safe in conjunction with lazy evaluation -- the unify code could be fooled about the present theory context);