disallow non-linear declaration patterns even when an exception is raised

this commit just changes the semantics of evaluate_dec; some proofs are
broken.