diff --git a/sledge/src/fol/arithmetic.ml b/sledge/src/fol/arithmetic.ml
index 9edf08f68..5110eab19 100644
--- a/sledge/src/fol/arithmetic.ml
+++ b/sledge/src/fol/arithmetic.ml
@@ -298,7 +298,10 @@ struct
           Sum.iter poly ~f:(fun mono _ ->
               if not (Mono.equal_one mono) then f mono ) )
 
-    let trms poly = Iter.flat_map ~f:Mono.trms (monos poly)
+    let trms poly =
+      match get_mono poly with
+      | Some mono -> Mono.trms mono
+      | None -> Iter.map ~f:trm_of_mono (monos poly)
 
     let map poly ~f =
       [%trace]
diff --git a/sledge/src/fol/arithmetic_intf.ml b/sledge/src/fol/arithmetic_intf.ml
index 0c768d13a..9bd81cc6a 100644
--- a/sledge/src/fol/arithmetic_intf.ml
+++ b/sledge/src/fol/arithmetic_intf.ml
@@ -59,7 +59,13 @@ module type S = sig
   (** Traverse *)
 
   val trms : t -> trm iter
-  (** [trms a] enumerates the indeterminate terms appearing in [a] *)
+  (** [trms a] is the maximal foreign or noninterpreted proper subterms of
+      [a]. Considering an arithmetic term as a polynomial,
+      [trms (c × (Σᵢ₌₁ⁿ cᵢ × Πⱼ₌₁ᵐᵢ
+      Xᵢⱼ^pᵢⱼ))] is the sequence of monomials
+      [Πⱼ₌₁ᵐᵢ Xᵢⱼ^pᵢⱼ] for each [i]. If the arithmetic
+      term is a monomial, [trms (Πⱼ₌₁ᵐ Xⱼ^pⱼ)] is the sequence
+      of factors [Xⱼ] for each [j]. *)
 
   val map : t -> f:(trm -> trm) -> t
   (** [map ~f a] is [a] with each maximal non-interpreted subterm