diff --git a/sledge/lib/domain_used_globals.ml b/sledge/lib/domain_used_globals.ml
index a6f4f8b92..e875c8d7a 100644
--- a/sledge/lib/domain_used_globals.ml
+++ b/sledge/lib/domain_used_globals.ml
@@ -25,7 +25,7 @@ let retn _ _ from_call post = Reg.Set.union from_call post
 let dnf t = [t]
 
 let add_if_global gs v =
-  if Var.global (Reg.var v) then Reg.Set.add gs v else gs
+  if Var.is_global (Reg.var v) then Reg.Set.add gs v else gs
 
 let used_globals ?(init = empty) exp =
   Exp.fold_regs exp ~init ~f:add_if_global
diff --git a/sledge/lib/exp.ml b/sledge/lib/exp.ml
index be83b6615..87aebff8d 100644
--- a/sledge/lib/exp.ml
+++ b/sledge/lib/exp.ml
@@ -147,7 +147,7 @@ let rec pp fs exp =
     match exp.desc with
     | Reg {name} -> (
       match Var.of_term exp.term with
-      | Some v when Var.global v -> pf "%@%s" name
+      | Some v when Var.is_global v -> pf "%@%s" name
       | _ -> pf "%%%s" name )
     | Nondet {msg} -> pf "nondet \"%s\"" msg
     | Label {name} -> pf "%s" name
diff --git a/sledge/lib/global.ml b/sledge/lib/global.ml
index a095996a1..966314600 100644
--- a/sledge/lib/global.ml
+++ b/sledge/lib/global.ml
@@ -28,6 +28,6 @@ let invariant g =
   @@ fun () ->
   let {reg; typ} = g in
   assert (Typ.is_sized typ) ;
-  assert (Var.global (Reg.var reg))
+  assert (Var.is_global (Reg.var reg))
 
 let mk ?init reg typ loc = {reg; init; typ; loc} |> check invariant
diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index 1b412bd67..db243c756 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -320,7 +320,7 @@ module Var = struct
 
   let id = function Var v -> v.id | x -> violates invariant x
   let name = function Var v -> v.name | x -> violates invariant x
-  let global = function Var v -> v.id = -1 | x -> violates invariant x
+  let is_global = function Var v -> v.id = -1 | x -> violates invariant x
   let of_ = function Var _ as v -> v | _ -> invalid_arg "Var.of_"
 
   let of_term = function
diff --git a/sledge/lib/term.mli b/sledge/lib/term.mli
index b952d945b..d29e3de48 100644
--- a/sledge/lib/term.mli
+++ b/sledge/lib/term.mli
@@ -117,12 +117,12 @@ module Var : sig
 
   include Invariant.S with type t := t
 
+  val name : t -> string
+  val is_global : t -> bool
   val of_ : term -> t
   val of_term : term -> t option
   val program : ?global:unit -> string -> t
   val fresh : string -> wrt:Set.t -> t * Set.t
-  val name : t -> string
-  val global : t -> bool
 
   module Subst : sig
     type var := t