kframework/k — pull request #827 by radumereuta (2014-08-11 21:38:08+00:00)
Title: Started to remove #String from the front end.

@yilongli I've started this in order to fix #789.
I tried a small example, and it still worked, although I'm pretty sure ktest is going to fail.
I think this should be enough for the front end. If not, then we could meet tomorrow and sort it out.