fix nontermination bug if loading definition in maude had errors
Java backend: added option --pattern-matching to krun
Merge pull request #476 from dwightguth/maudetask

fix nontermination bug if loading definition in maude had errors
Java backend: added tag interface for data structure choice operations; fixed a related latent bug
Java backend: fixed a few bugs in SetLookup & PatternMatcher
Java backend: used GroundRewriter for run/search when option --pattern-matching is enabled
Java backend: added tag interface for data structure update operations
Java backend: used pattern-matching instead of unification when evaluating user-defined functions
Java backend: fixed a few bugs in PatternMatcher; revised it to allow non-ground subject term
used simple-typed-dynamic, kool-typed-static/dynamic, and fun-untyped to test pattern matching in regression test
Java backend: commented out an assertion that will fail on logik.k
fixed broken rebase; added -d option to kompile and krun for testing pattern-matching
fixed missing copyright info during rebasing
removed an opt. that doesn't apply to unification because variables of a rule can end up in the constraint rather than in substitution form; and they must be renamed
fixed the computation of unbound variables of a rule
minor refactorings; more comments
a few things: 1) renamed variables when neccessary; 2) applied owise'' rule conservatively; 3) revised assertion message
fixed a latent bug due to variable interference
fixed errors occured after rebasing
fixed broken options