Maybe the relevant change is that definitions are now by default irreducible and I'm pretty sure that this change was between 4.1 and 4.12. So you have to tell simp explicitly to unfold the definition of xs now.

def xs := [1]
theorem xs_not_empty : xs.length > 0 := by simp [xs]

works fine.