_unint proof tactics don't work for constants defined in .saw files

[brianhuffman]

We have two ways to represent a defined constant in a saw-core Term: First there is GlobalDef, which refers to a definition in a saw-core module; occurrences are created with scGlobalDef or scGlobalApply. Second there is Constant, which is defined dynamically with scConstant.

As it turns out, the uninterpreted function feature of saw-script proof tactics only works with Constant terms, and not GlobalDef ones. So, for example, while it is possible to treat the cryptol pmod and pmult operators as uninterpreted (as they are defined in the Cryptol prelude and translated with scConstant) we can't make >>> uninterpreted (because it's a Cryptol primitive that is translated with scGlobalDef).

We should make all of this more consistent. We could make the saw-core simulator backend handle GlobalDef the same way as Constant. Or else we could just unify GlobalDef and Constant, because we don't really need both.

[brianhuffman]

Fixed by GaloisInc/saw-core#118, which was included in saw-script by PR #1020.