diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 187dbc475..1a00261e7 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -508,15 +508,18 @@ let rec canon_extend_ a x =
     | None -> (
         (* norm wrt rep and add subterms *)
         let a_norm, x = Trm.fold_map ~f:canon_extend_ a x in
-        match Trm.Map.find_or_add a_norm a_norm x.rep with
-        | Some a', _ ->
-            (* a_norm already equal to a' *)
-            (a', x)
-        | None, rep ->
-            (* a_norm newly added *)
-            let use = add_uses_of a_norm x.use in
-            let x = {x with rep; use} in
-            (a_norm, x) ) )
+        match Theory.classify a_norm with
+        | InterpAtom | NonInterpAtom | InterpApp -> canon_extend_ a_norm x
+        | UninterpApp -> (
+          match Trm.Map.find_or_add a_norm a_norm x.rep with
+          | Some a', _ ->
+              (* a_norm already equal to a' *)
+              (a', x)
+          | None, rep ->
+              (* a_norm newly added *)
+              let use = add_uses_of a_norm x.use in
+              let x = {x with rep; use} in
+              (a_norm, x) ) ) )
 
 (** normalize and add a term to the carrier *)
 let canon_extend a x =
diff --git a/sledge/src/fol/theory.ml b/sledge/src/fol/theory.ml
index a47ce9592..a5ef78136 100644
--- a/sledge/src/fol/theory.ml
+++ b/sledge/src/fol/theory.ml
@@ -32,9 +32,13 @@ let pp ppf = function
 (* Classification of terms ================================================*)
 
 type kind = InterpApp | NonInterpAtom | InterpAtom | UninterpApp
-[@@deriving compare, equal]
+[@@deriving compare, equal, sexp_of]
 
 let classify e =
+  [%trace]
+    ~call:(fun {pf} -> pf "%a" Trm.pp e)
+    ~retn:(fun {pf} k -> pf "%a" Sexp.pp (sexp_of_kind k))
+  @@ fun () ->
   match (e : Trm.t) with
   | Var _ -> NonInterpAtom
   | Z _ | Q _ -> InterpAtom