The superposition calculus has been formalized in Isabelle/HOL twice before but both times without a type system. By contrast, modern superposition provers do support types. We extend an existing Isabelle formalization of superposition with simple monomorphic types, or sorts. This extension is straightforward on paper but surprisingly intricate to carry out formally. We also use this opportunity to refactor the proof text to avoid quadruplicated definitions, lemmas, and proofs about terms, atoms, literals, and clauses. The extended formalization and its refactoring benefit from Isabelle’s locales, structured Isar proofs, and Sledgehammer proof tool.