diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml
index d7ca83147..07b03a1bc 100644
--- a/sledge/lib/equality.ml
+++ b/sledge/lib/equality.ml
@@ -422,7 +422,7 @@ let congruent r a b =
 let lookup r a =
   [%Trace.call fun {pf} -> pf "%a@ %a" Term.pp a pp r]
   ;
-  ( Base.With_return.with_return
+  ( with_return
   @@ fun {return} ->
   (* congruent specialized to assume [a] canonized and [b] non-interpreted *)
   let semi_congruent r a b =
@@ -479,7 +479,7 @@ let merge us a b r =
 
 (** find an unproved equation between congruent terms *)
 let find_missing r =
-  Base.With_return.with_return
+  with_return
   @@ fun {return} ->
   Subst.iteri r.rep ~f:(fun ~key:a ~data:a' ->
       Subst.iteri r.rep ~f:(fun ~key:b ~data:b' ->
diff --git a/sledge/lib/import/IArray.ml b/sledge/lib/import/IArray.ml
index 12dacd1be..d0bc26af2 100644
--- a/sledge/lib/import/IArray.ml
+++ b/sledge/lib/import/IArray.ml
@@ -7,9 +7,9 @@
 
 (** IArray - Immutable view of an array *)
 
+open Import0
 module Array = Base.Array
 module Hash = Base.Hash
-module With_return = Base.With_return
 open Base.Continue_or_stop
 
 (** = 'a array but covariant since imperative operations hidden *)
@@ -108,7 +108,7 @@ let fold_map x ~init ~f =
   (s, v x)
 
 let fold_map_until xs ~init ~f ~finish =
-  With_return.with_return (fun {return} ->
+  with_return (fun {return} ->
       finish
         (fold_map xs ~init ~f:(fun s x ->
              match f s x with Continue x -> x | Stop x -> return x )) )
diff --git a/sledge/lib/import/import0.ml b/sledge/lib/import/import0.ml
index 8f4733599..4c87d7c34 100644
--- a/sledge/lib/import/import0.ml
+++ b/sledge/lib/import/import0.ml
@@ -66,3 +66,10 @@ module type OrderedType = sig
 end
 
 exception Duplicate
+
+module Return = struct type 'r t = {return: 'a. 'r -> 'a} [@@unboxed] end
+
+let with_return (type a) f =
+  let module M = struct exception Return of a end in
+  let return a = raise_notrace (M.Return a) in
+  try f {Return.return} with M.Return a -> a
diff --git a/sledge/lib/import/list.ml b/sledge/lib/import/list.ml
index 258484bac..d84beb559 100644
--- a/sledge/lib/import/list.ml
+++ b/sledge/lib/import/list.ml
@@ -5,6 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
+open Import0
 include Base.List
 
 let rec pp ?pre ?suf sep pp_elt fs = function
@@ -30,7 +31,7 @@ let find_map_remove xs ~f =
   find_map_remove_ [] xs
 
 let fold_option xs ~init ~f =
-  Base.With_return.with_return
+  with_return
   @@ fun {return} ->
   Some
     (fold xs ~init ~f:(fun acc elt ->