diff --git a/src/AlphaLibMacros.cppo.ml b/src/AlphaLibMacros.cppo.ml
index 7bdd2d78f60a62d6aa5516c996832745ea92e2d0..05a22ba1c0ff0230d4fa2a8c8083895a2426ac5a 100644
--- a/src/AlphaLibMacros.cppo.ml
+++ b/src/AlphaLibMacros.cppo.ml
@@ -7,29 +7,9 @@
 
 (* -------------------------------------------------------------------------- *)
 
-(* [fa] could be defined in terms of [reduce], as follows. *)
-
 #define FA_CLASS     __fa
 #define FA_FUN(term) CONCAT(fa_, term)
 
-#define __FA                                                                   \
-  class FA_CLASS = object                                                      \
-    inherit [_] reduce                                                         \
-    inherit [_] KitFa.reduce                                                   \
-  end                                                                          \
-
-#define FA(term)                                                               \
-  let FA_FUN(term) t =                                                         \
-    new FA_CLASS # VISIT(term) () t                                            \
-
-#undef __FA
-#undef FA
-
-(* -------------------------------------------------------------------------- *)
-
-(* We prefer to define [fa] in terms of [iter] because we wish to eliminate
-   our dependency on [reduce] visitors. *)
-
 #define __FA                                                                   \
   class FA_CLASS = object                                                      \
     inherit [_] iter                                                           \
diff --git a/src/KitFa.ml b/src/KitFa.ml
index 39d9e8782daef6de9af1dfa165dfdb8619c0c4ef..97a24be6677ff95ab83937c4e63300eec0f43d95 100644
--- a/src/KitFa.ml
+++ b/src/KitFa.ml
@@ -62,29 +62,6 @@ end
 
 (* -------------------------------------------------------------------------- *)
 
-(* Computing the free atoms of a term, via [reduce]. *)
-
-(* In this style, no environment is required. *)
-
-(* type env = unit *)
-
-class ['self] reduce = object (_ : 'self)
-
-  (* The monoid of sets of atoms is used. *)
-  inherit [_] Atom.Set.union_monoid
-
-  method private extend _x () = ()
-
-  (* The atom [x] is removed from the set of free atoms when the scope of [x]
-     is exited. *)
-  method private restrict = Atom.Set.remove
-
-  method private visit_'fn () x = Atom.Set.singleton x
-
-end
-
-(* -------------------------------------------------------------------------- *)
-
 (* Testing whether a term has a free atom that satisfies a predicate [p]. *)
 
 exception Found of Atom.t
diff --git a/src/attic/KitFa.ml b/src/attic/KitFa.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9a76f00e69d908d911b04aa7fb3e76f6e538c0e1
--- /dev/null
+++ b/src/attic/KitFa.ml
@@ -0,0 +1,34 @@
+(* -------------------------------------------------------------------------- *)
+
+(* Computing the free atoms of a term, via [reduce]. *)
+
+(* In this style, no environment is required. *)
+
+(* type env = unit *)
+
+class ['self] reduce = object (_ : 'self)
+
+  (* The monoid of sets of atoms is used. *)
+  inherit [_] Atom.Set.union_monoid
+
+  method private extend _x () = ()
+
+  (* The atom [x] is removed from the set of free atoms when the scope of [x]
+     is exited. *)
+  method private restrict = Atom.Set.remove
+
+  method private visit_'fn () x = Atom.Set.singleton x
+
+end
+
+(* -------------------------------------------------------------------------- *)
+
+#define __FA                                                                   \
+  class FA_CLASS = object                                                      \
+    inherit [_] reduce                                                         \
+    inherit [_] KitFa.reduce                                                   \
+  end                                                                          \
+
+#define FA(term)                                                               \
+  let FA_FUN(term) t =                                                         \
+    new FA_CLASS # VISIT(term) () t                                            \