I am a happy user of Isabelle/Isar and Sledgehammer, but am just now trying to also use locales, as in my use case there are just overwhelming arguments for it.
I am using the Isabelle/December 2021 distribution, but most of the time when I am trying to use sledgehammer within a locale context, I will get a message like this:
"cvc4": Prover error:
exception TERM raised (line 457 of "~~/src/HOL/Tools/SMT/smt_translate.ML"): bad SMT term
It is the same message for other provers as well. Is this something that is a well-known problem? Without using locales I had such a problem only come up when my theory name was confused with some HOL theory name, and renaming my theory was a workaround. Is there something similar at play here? Is there an easy fix? Because I use sledgehammer a lot, so not being able to use it within a locale would be a severe blow against using locales.
For the sake of completeness, a summary of the discussion on the Isabelle mailing-list.
There is an issue in the translation from Isabelle to SMT Lib (the language for SMT solvers): lets inside lets are not translated correctly. This should be fixed in the next Isabelle release.
The work-around in the mean time is to avoid let inside let.