kframework/k — pull request #653 by traiansf (2014-06-23 22:17:55+00:00)
Title: Issue 607

Apparently there were some issues with the substitution when using bounded symbolic variables. Not sure why these were not caught by the lambda tests. To address them, I had to force syntactic equality in the process of computing the free variables. The main thing I'm not proud of is basically changing the definition of -Set to a syntactic one (by abusing ==K true). @andreistefanescu says that is probably ok. If anybody objects to that, I can create a -SetSyn or something similar for syntactic difference.

@andreistefanescu @grosu @dwightguth please review.