diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml
index f66044edf..21c41433e 100644
--- a/sledge/src/fol/trm.ml
+++ b/sledge/src/fol/trm.ml
@@ -94,27 +94,6 @@ end = struct
     | Apply of Funsym.t * t array
   [@@deriving compare, equal, sexp]
 
-  module Var1 = struct
-    module T = struct
-      type nonrec t = t [@@deriving compare, equal, sexp]
-
-      let invariant x =
-        let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
-        match x with
-        | Var _ -> ()
-        | _ -> fail "non-var: %a" Sexp.pp_hum (sexp_of_t x) ()
-
-      let make ~id ~name = Var {id; name} |> check invariant
-      let id = function Var v -> v.id | x -> violates invariant x
-      let name = function Var v -> v.name | x -> violates invariant x
-    end
-
-    include Var0.Make (T)
-
-    let of_ v = v |> check T.invariant
-    let of_trm = function Var _ as v -> Some v | _ -> None
-  end
-
   (* nul-terminated string value represented by a concatenation *)
   let string_of_concat xs =
     let exception Not_a_string in
@@ -174,6 +153,27 @@ end = struct
 
   let pp = ppx (fun _ -> None)
 
+  module Var1 = struct
+    module T = struct
+      type nonrec t = t [@@deriving compare, equal, sexp]
+
+      let invariant x =
+        let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
+        match x with
+        | Var _ -> ()
+        | _ -> fail "non-var: %a" Sexp.pp_hum (sexp_of_t x) ()
+
+      let make ~id ~name = Var {id; name} |> check invariant
+      let id = function Var v -> v.id | x -> violates invariant x
+      let name = function Var v -> v.name | x -> violates invariant x
+    end
+
+    include Var0.Make (T)
+
+    let of_ v = v |> check T.invariant
+    let of_trm = function Var _ as v -> Some v | _ -> None
+  end
+
   let invariant e =
     let@ () = Invariant.invariant [%here] e [%sexp_of: t] in
     match e with
diff --git a/sledge/src/fol/trm.mli b/sledge/src/fol/trm.mli
index f6de238fc..c821fe7ef 100644
--- a/sledge/src/fol/trm.mli
+++ b/sledge/src/fol/trm.mli
@@ -25,6 +25,8 @@ type t = private
   | Apply of Funsym.t * t array
 [@@deriving compare, equal, sexp]
 
+module Arith : Arithmetic.S with type trm := t with type t = arith
+
 module Var : sig
   type trm := t
 
@@ -34,8 +36,6 @@ module Var : sig
   val of_trm : trm -> t option
 end
 
-module Arith : Arithmetic.S with type trm := t with type t = arith
-
 module Set : sig
   include Set.S with type elt := t