Allow me to send an immediate bugfix. I thought I was being clever by replacing HOL conjunction with Pure conjunction in the output of split_simps, but it appears that the simplifier doesn't know what to do with it. Redefining conjunct_rules like this fixes it: val conjunct_rules = foldr1 (fn (a, b) => [a, b] MRS conjI); The reason for this is that theorem-modifying attributes don't seem to be able to emit a list of theorems, so I had to fold the theorems back into a single one. Perhaps the isabelle developers can think of a better way. I attach the newest version. Yours, Thomas.