diff --git a/backend/cn/lib/cLogicalFuns.ml b/backend/cn/lib/cLogicalFuns.ml
index b805031f6..fde6f7448 100644
--- a/backend/cn/lib/cLogicalFuns.ml
+++ b/backend/cn/lib/cLogicalFuns.ml
@@ -714,8 +714,8 @@ let c_fun_to_it id_loc glob_context (id : Sym.t) fsym def (fn : 'bty Mu.fun_map_
 let upd_def (loc, sym, def_tm) =
   let open Definition.Function in
   let@ def = get_logical_function_def loc sym in
-  match def.definition with
-  | Uninterp -> add_logical_function sym { def with definition = Def def_tm }
+  match def.body with
+  | Uninterp -> add_logical_function sym { def with body = Def def_tm }
   | _ ->
     fail_n
       { loc;
diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml
index b9fd514d1..3f0d54d36 100644
--- a/backend/cn/lib/check.ml
+++ b/backend/cn/lib/check.ml
@@ -2230,7 +2230,7 @@ let record_and_check_logical_functions funs =
   let@ () =
     ListM.iterM
       (fun (name, def) ->
-        let@ simple_def = WellTyped.WLFD.welltyped { def with definition = Uninterp } in
+        let@ simple_def = WellTyped.WLFD.welltyped { def with body = Uninterp } in
         add_logical_function name simple_def)
       recursive
   in
diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml
index ac88aa73f..203f5a0d8 100644
--- a/backend/cn/lib/cn_internal_to_ail.ml
+++ b/backend/cn/lib/cn_internal_to_ail.ml
@@ -2932,7 +2932,7 @@ let rec generate_record_opt pred_sym = function
 
 (* TODO: Finish with rest of function - maybe header file with A.Decl_function (cn.h?) *)
 let cn_to_ail_function_internal
-  (fn_sym, (lf_def : Definition.Function.definition))
+  (fn_sym, (lf_def : Definition.Function.t))
   (cn_datatypes : A.sigma_cn_datatype list)
   (cn_functions : A.sigma_cn_function list)
   : ((Locations.t * A.sigma_declaration)
@@ -2942,7 +2942,7 @@ let cn_to_ail_function_internal
   let ret_type = bt_to_ail_ctype ~pred_sym:(Some fn_sym) lf_def.return_bt in
   (* let ret_type = mk_ctype C.(Pointer (empty_qualifiers, ret_type)) in *)
   let bs, ail_func_body_opt =
-    match lf_def.definition with
+    match lf_def.body with
     | Def it | Rec_Def it ->
       let bs, ss =
         cn_to_ail_expr_internal_with_pred_name (Some fn_sym) cn_datatypes [] it Return
diff --git a/backend/cn/lib/cn_internal_to_ail.mli b/backend/cn/lib/cn_internal_to_ail.mli
index 0840c8515..0eab96128 100644
--- a/backend/cn/lib/cn_internal_to_ail.mli
+++ b/backend/cn/lib/cn_internal_to_ail.mli
@@ -148,7 +148,7 @@ val cn_to_ail_records
   A.sigma_tag_definition list
 
 val cn_to_ail_function_internal
-  :  Sym.t * Definition.Function.definition ->
+  :  Sym.t * Definition.Function.t ->
   A.sigma_cn_datatype list ->
   A.sigma_cn_function list ->
   ((Locations.t * A.sigma_declaration)
diff --git a/backend/cn/lib/compile.ml b/backend/cn/lib/compile.ml
index 4424446d8..94c498f0c 100644
--- a/backend/cn/lib/compile.ml
+++ b/backend/cn/lib/compile.ml
@@ -1218,7 +1218,7 @@ let translate_cn_function env (def : cn_function) =
             })
       def.cn_func_attrs
   in
-  let@ definition =
+  let@ body =
     match def.cn_func_body with
     | Some body ->
       let@ body = translate_cn_func_body env' body in
@@ -1232,7 +1232,7 @@ let translate_cn_function env (def : cn_function) =
         args = List.map_snd SBT.proj args;
         return_bt = SBT.proj return_bt;
         emit_coq = not coq_unfold;
-        definition
+        body
       }
   in
   return (def.cn_func_name, def2)
@@ -1380,7 +1380,7 @@ let translate_cn_clauses env clauses =
         Pure.handle "Predicate guards" (ET.translate_cn_expr Sym.Set.empty env e_)
       in
       let@ cl = translate_cn_clause env cl_ in
-      self (Def.{ loc; guard = IT.Surface.proj e; packing_ft = cl } :: acc) clauses'
+      self ({ loc; guard = IT.Surface.proj e; packing_ft = cl } :: acc) clauses'
   in
   let@ xs = self [] clauses in
   return (List.rev xs)
diff --git a/backend/cn/lib/context.ml b/backend/cn/lib/context.ml
index 8e5d57e3f..5f6256f4c 100644
--- a/backend/cn/lib/context.ml
+++ b/backend/cn/lib/context.ml
@@ -280,7 +280,7 @@ let not_given_to_solver ctxt =
   let preds =
     Sym.Map.bindings
       (Sym.Map.filter
-         (fun _ v -> not (Definition.given_to_solver v))
+         (fun _ v -> not (Definition.Predicate.given_to_solver v))
          global.resource_predicates)
   in
   (constraints, funs, preds)
diff --git a/backend/cn/lib/definition.ml b/backend/cn/lib/definition.ml
index e8c3ea11b..728947d3f 100644
--- a/backend/cn/lib/definition.ml
+++ b/backend/cn/lib/definition.ml
@@ -3,33 +3,33 @@ module AT = ArgumentTypes
 module LAT = LogicalArgumentTypes
 
 module Function = struct
-  type def_or_uninterp =
+  type body =
     | Def of IT.t
     | Rec_Def of IT.t
     | Uninterp
 
-  let subst_def_or_uninterp subst = function
+  let subst_body subst = function
     | Def it -> Def (IT.subst subst it)
     | Rec_Def it -> Rec_Def (IT.subst subst it)
     | Uninterp -> Uninterp
 
 
-  type definition =
+  type t =
     { loc : Locations.t;
       args : (Sym.t * BaseTypes.t) list;
       (* If the predicate is supposed to get used in a quantified form, one of the arguments
          has to be the index/quantified variable. For now at least. *)
       return_bt : BaseTypes.t;
       emit_coq : bool;
-      definition : def_or_uninterp
+      body : body
     }
 
   let is_recursive def =
-    match def.definition with Rec_Def _ -> true | Def _ -> false | Uninterp -> false
+    match def.body with Rec_Def _ -> true | Def _ -> false | Uninterp -> false
 
 
   let given_to_solver def =
-    match def.definition with Rec_Def _ -> false | Def _ -> true | Uninterp -> false
+    match def.body with Rec_Def _ -> false | Def _ -> true | Uninterp -> false
 
 
   let pp_args xs =
@@ -39,71 +39,39 @@ module Function = struct
       xs
 
 
-  let pp_def nm def =
+  let pp nm def =
     let open Pp in
     nm
     ^^ colon
     ^^^ pp_args def.args
     ^^ colon
     ^/^
-    match def.definition with
+    match def.body with
     | Uninterp -> !^"uninterpreted"
     | Def t -> IT.pp t
     | Rec_Def t -> !^"rec:" ^^^ IT.pp t
 
 
-  let open_fun def_args def_body args =
+  let open_ def_args def_body args =
     let su = IT.make_subst (List.map2 (fun (s, _) arg -> (s, arg)) def_args args) in
     IT.subst su def_body
 
 
   let unroll_once def args =
-    match def.definition with
-    | Def body | Rec_Def body -> Some (open_fun def.args body args)
+    match def.body with
+    | Def body | Rec_Def body -> Some (open_ def.args body args)
     | Uninterp -> None
 
 
-  let try_open_fun def args =
-    match def.definition with
-    | Def body -> Some (open_fun def.args body args)
+  let try_open def args =
+    match def.body with
+    | Def body -> Some (open_ def.args body args)
     | Rec_Def _ -> None
     | Uninterp -> None
 
 
-  (* let try_open_fun_to_term def name args = Option.map (fun body -> Body.to_term
-     def.return_bt body ) (try_open_fun def name args) *)
-
-  (* let add_unfolds_to_terms preds terms = let rec f acc t = match IT.term t with |
-     IT.Apply (name, ts) -> let def = Sym.Map.find name preds in begin match
-     try_open_fun_to_term def name ts with | None -> acc | Some t2 -> f (t2 :: acc) t2 end |
-     _ -> acc in IT.fold_list (fun _ acc t -> f acc t) [] terms terms *)
-
-  (* (\* Check for cycles in the logical predicate graph, which would cause *)
-  (*    the system to loop trying to unfold them. Predicates whose definition *)
-  (*    are marked with Rec_Def aren't checked, as cycles there are expected. *\) *)
-  (* let cycle_check (defs : definition Sym.Map.t) = *)
-  (*   let def_preds nm =  *)
-  (*     let def =  Sym.Map.find nm defs in *)
-  (*     begin match def.definition with *)
-  (*     | Def t -> Sym.Set.elements (IT.preds_of (Body.to_term def.return_bt t)) *)
-  (*     | _ -> [] *)
-  (*     end *)
-  (*   in *)
-  (*   let rec search known_ok = function *)
-  (*     | [] -> None *)
-  (*     | (nm, Some path) :: q -> if Sym.Set.mem nm known_ok *)
-  (*       then search known_ok q *)
-  (*       else if List.exists (Sym.equal nm) path *)
-  (*       then Some (List.rev path @ [nm]) *)
-  (*       else *)
-  (*         let deps = List.map (fun p -> (p, Some (nm :: path))) (def_preds nm) in *)
-  (*         search known_ok (deps @ [(nm, None)] @ q) *)
-  (*     | (nm, None) :: q -> search (Sym.Set.add nm known_ok) q *)
-  (* in search Sym.Set.empty (List.map (fun (p, _) -> (p, Some [])) (Sym.Map.bindings
-     defs)) *)
-
   (*Extensibility hook. For now, all functions are displayed as "interesting" in error reporting*)
-  let is_interesting : definition -> bool = fun _ -> true
+  let is_interesting : t -> bool = fun _ -> true
 end
 
 module Clause = struct
@@ -160,6 +128,53 @@ module Predicate = struct
           (match def.clauses with
            | Some clauses -> Pp.list Clause.pp clauses
            | None -> !^"(uninterpreted)")
+
+
+  let instantiate (def : t) ptr_arg iargs =
+    match def.clauses with
+    | Some clauses ->
+      let subst =
+        IT.make_subst
+          ((def.pointer, ptr_arg)
+           :: List.map2 (fun (def_ia, _) ia -> (def_ia, ia)) def.iargs iargs)
+      in
+      Some (List.map (Clause.subst subst) clauses)
+    | None -> None
+
+
+  let identify_right_clause provable (def : t) pointer iargs =
+    match instantiate def pointer iargs with
+    | None ->
+      (* "uninterpreted" predicates cannot be un/packed *)
+      None
+    | Some clauses ->
+      let rec try_clauses : Clause.t list -> _ = function
+        | [] -> None
+        | clause :: clauses ->
+          (match provable (LogicalConstraints.T clause.guard) with
+           | `True -> Some clause
+           | `False ->
+             let loc = Locations.other __FUNCTION__ in
+             (match provable (LogicalConstraints.T (IT.not_ clause.guard loc)) with
+              | `True -> try_clauses clauses
+              | `False ->
+                Pp.debug
+                  5
+                  (lazy
+                    (Pp.item "cannot prove or disprove clause guard" (IT.pp clause.guard)));
+                None))
+      in
+      try_clauses clauses
+
+
+  (* determines if a resource predicate will be given to the solver
+   *    TODO: right now this is an overapproximation *)
+  let given_to_solver (def : t) =
+    match def.clauses with
+    | None -> false
+    | Some [] -> true
+    | Some [ _ ] -> true
+    | _ -> false
 end
 
 let alloc =
@@ -172,52 +187,5 @@ let alloc =
     }
 
 
-let instantiate_clauses (def : Predicate.t) ptr_arg iargs =
-  match def.clauses with
-  | Some clauses ->
-    let subst =
-      IT.make_subst
-        ((def.pointer, ptr_arg)
-         :: List.map2 (fun (def_ia, _) ia -> (def_ia, ia)) def.iargs iargs)
-    in
-    Some (List.map (Clause.subst subst) clauses)
-  | None -> None
-
-
-let identify_right_clause provable (def : Predicate.t) pointer iargs =
-  match instantiate_clauses def pointer iargs with
-  | None ->
-    (* "uninterpreted" predicates cannot be un/packed *)
-    None
-  | Some clauses ->
-    let rec try_clauses : Clause.t list -> _ = function
-      | [] -> None
-      | clause :: clauses ->
-        (match provable (LogicalConstraints.T clause.guard) with
-         | `True -> Some clause
-         | `False ->
-           let loc = Locations.other __FUNCTION__ in
-           (match provable (LogicalConstraints.T (IT.not_ clause.guard loc)) with
-            | `True -> try_clauses clauses
-            | `False ->
-              Pp.debug
-                5
-                (lazy
-                  (Pp.item "cannot prove or disprove clause guard" (IT.pp clause.guard)));
-              None))
-    in
-    try_clauses clauses
-
-
-(* determines if a resource predicate will be given to the solver
-   TODO: right now this is an overapproximation *)
-let given_to_solver (def : Predicate.t) =
-  match def.clauses with
-  | None -> false
-  | Some [] -> true
-  | Some [ _ ] -> true
-  | _ -> false
-
-
 (*Extensibility hook. For now, all predicates are displayed as "interesting" in error reporting*)
 let is_interesting : Predicate.t -> bool = fun _ -> true
diff --git a/backend/cn/lib/definition.mli b/backend/cn/lib/definition.mli
new file mode 100644
index 000000000..5feaa9c77
--- /dev/null
+++ b/backend/cn/lib/definition.mli
@@ -0,0 +1,73 @@
+module Function : sig
+  type body =
+    | Def of IndexTerms.t
+    | Rec_Def of IndexTerms.t
+    | Uninterp
+
+  val subst_body : [ `Rename of Sym.t | `Term of IndexTerms.t ] Subst.t -> body -> body
+
+  type t =
+    { loc : Locations.t;
+      args : (Sym.t * BaseTypes.t) list;
+      return_bt : BaseTypes.t;
+      emit_coq : bool;
+      body : body
+    }
+
+  val is_recursive : t -> bool
+
+  val given_to_solver : t -> bool
+
+  val pp_args : (Cerb_frontend.Symbol.sym * unit BaseTypes.t_gen) list -> Pp.document
+
+  val pp : Pp.document -> t -> Pp.document
+
+  val open_ : (Sym.t * 'a) list -> IndexTerms.t -> IndexTerms.t list -> IndexTerms.t
+
+  val unroll_once : t -> IndexTerms.t list -> IndexTerms.t option
+
+  val try_open : t -> IndexTerms.t list -> IndexTerms.t option
+
+  val is_interesting : t -> bool
+end
+
+module Clause : sig
+  type t =
+    { loc : Locations.t;
+      guard : IndexTerms.t;
+      packing_ft : LogicalArgumentTypes.packing_ft
+    }
+
+  val pp : t -> Pp.document
+
+  val subst : [ `Rename of Sym.t | `Term of IndexTerms.t ] Subst.t -> t -> t
+
+  val lrt : IndexTerms.t -> IndexTerms.t LogicalArgumentTypes.t -> LogicalReturnTypes.t
+end
+
+module Predicate : sig
+  type t =
+    { loc : Locations.t;
+      pointer : Sym.t;
+      iargs : (Sym.t * BaseTypes.t) list;
+      oarg_bt : BaseTypes.t;
+      clauses : Clause.t list option
+    }
+
+  val pp : t -> Pp.document
+
+  val instantiate : t -> IndexTerms.t -> IndexTerms.t list -> Clause.t list option
+
+  val identify_right_clause
+    :  (LogicalConstraints.logical_constraint -> [< `False | `True ]) ->
+    t ->
+    IndexTerms.t ->
+    IndexTerms.t list ->
+    Clause.t option
+
+  val given_to_solver : t -> bool
+end
+
+val alloc : Predicate.t
+
+val is_interesting : Predicate.t -> bool
diff --git a/backend/cn/lib/executable_spec_internal.ml b/backend/cn/lib/executable_spec_internal.ml
index f6cf6d066..d1cb0a530 100644
--- a/backend/cn/lib/executable_spec_internal.ml
+++ b/backend/cn/lib/executable_spec_internal.ml
@@ -353,8 +353,7 @@ let bt_is_record_or_tuple = function BT.Record _ | BT.Tuple _ -> true | _ -> fal
 let fns_and_preds_with_record_rt (funs, preds) =
   let funs' =
     List.filter
-      (fun (_, (def : Definition.Function.definition)) ->
-        bt_is_record_or_tuple def.return_bt)
+      (fun (_, (def : Definition.Function.t)) -> bt_is_record_or_tuple def.return_bt)
       funs
   in
   let fun_syms = List.map (fun (fn_sym, _) -> fn_sym) funs' in
@@ -369,7 +368,7 @@ let fns_and_preds_with_record_rt (funs, preds) =
 
 let generate_c_functions_internal
   (sigm : CF.GenTypes.genTypeCategory CF.AilSyntax.sigma)
-  (logical_predicates : (Sym.t * Definition.Function.definition) list)
+  (logical_predicates : (Sym.t * Definition.Function.t) list)
   =
   let ail_funs_and_records =
     List.map
diff --git a/backend/cn/lib/executable_spec_records.ml b/backend/cn/lib/executable_spec_records.ml
index f16abd0fe..1eb25410a 100644
--- a/backend/cn/lib/executable_spec_records.ml
+++ b/backend/cn/lib/executable_spec_records.ml
@@ -140,9 +140,7 @@ let rec populate ?cn_sym bt =
 
 let add_records_to_map_from_fns_and_preds cn_funs cn_preds =
   let fun_syms_and_ret_types =
-    List.map
-      (fun (sym, (def : Definition.Function.definition)) -> (sym, def.return_bt))
-      cn_funs
+    List.map (fun (sym, (def : Definition.Function.t)) -> (sym, def.return_bt)) cn_funs
   in
   let pred_syms_and_ret_types =
     List.map (fun (sym, (def : Definition.Predicate.t)) -> (sym, def.oarg_bt)) cn_preds
diff --git a/backend/cn/lib/explain.ml b/backend/cn/lib/explain.ml
index d9354a371..e42c39f12 100644
--- a/backend/cn/lib/explain.ml
+++ b/backend/cn/lib/explain.ml
@@ -353,7 +353,6 @@ let trace (ctxt, log) (model_with_q : Solver.model_with_q) (extras : state_extra
     match extras.request with
     | None -> []
     | Some req ->
-      let open Definition in
       (match Req.get_name req with
        | Owned _ -> []
        | PName pname ->
diff --git a/backend/cn/lib/global.ml b/backend/cn/lib/global.ml
index 630d5a472..3aa48779a 100644
--- a/backend/cn/lib/global.ml
+++ b/backend/cn/lib/global.ml
@@ -10,7 +10,7 @@ type t =
     datatype_order : Sym.t list list option;
     fun_decls : (Locations.t * AT.ft option * Sctypes.c_concrete_sig) Sym.Map.t;
     resource_predicates : Definition.Predicate.t Sym.Map.t;
-    logical_functions : Definition.Function.definition Sym.Map.t;
+    logical_functions : Definition.Function.t Sym.Map.t;
     lemmata : (Locations.t * AT.lemmat) Sym.Map.t
   }
 
diff --git a/backend/cn/lib/lemmata.ml b/backend/cn/lib/lemmata.ml
index dc44cebc5..e648918ba 100644
--- a/backend/cn/lib/lemmata.ml
+++ b/backend/cn/lib/lemmata.ml
@@ -407,8 +407,8 @@ let it_adjust (global : Global.t) it =
     | IT.Apply (name, args) ->
       let open Definition.Function in
       let def = Sym.Map.find name global.logical_functions in
-      (match (def.definition, def.emit_coq) with
-       | Def body, false -> f (open_fun def.args body args)
+      (match (def.body, def.emit_coq) with
+       | Def body, false -> f (open_ def.args body args)
        | _ -> t)
     | IT.Good (ct, t2) ->
       if Option.is_some (Sctypes.is_struct_ctype ct) then
@@ -781,7 +781,7 @@ let ensure_pred global list_mono loc name aux =
   let open Definition.Function in
   let def = Sym.Map.find name global.Global.logical_functions in
   let inf = (loc, Pp.typ (Pp.string "pred") (Sym.pp name)) in
-  match def.definition with
+  match def.body with
   | Uninterp ->
     gen_ensure
       1
@@ -852,10 +852,10 @@ let rec unfold_if_possible global it =
   match it with
   | IT (IT.Apply (name, args), _, _) ->
     let def = Option.get (Global.get_logical_function_def global name) in
-    (match def.definition with
+    (match def.body with
      | Rec_Def _ -> it
      | Uninterp -> it
-     | Def body -> unfold_if_possible global (open_fun def.args body args))
+     | Def body -> unfold_if_possible global (open_ def.args body args))
   | _ -> it
 
 
diff --git a/backend/cn/lib/mucore.ml b/backend/cn/lib/mucore.ml
index 538e636b1..6c417d27c 100644
--- a/backend/cn/lib/mucore.ml
+++ b/backend/cn/lib/mucore.ml
@@ -429,7 +429,7 @@ type 'TY file =
     stdlib_syms : Sym.Set.t;
     mk_functions : function_to_convert list;
     resource_predicates : (Sym.t * Definition.Predicate.t) list;
-    logical_predicates : (Sym.t * Definition.Function.definition) list;
+    logical_predicates : (Sym.t * Definition.Function.t) list;
     datatypes : (Sym.t * datatype) list;
     lemmata : (Sym.t * (Locations.t * ArgumentTypes.lemmat)) list;
     call_funinfo : (Sym.t, Sctypes.c_concrete_sig) Pmap.map
diff --git a/backend/cn/lib/mucore.mli b/backend/cn/lib/mucore.mli
index fac5c3c23..3d69d39c6 100644
--- a/backend/cn/lib/mucore.mli
+++ b/backend/cn/lib/mucore.mli
@@ -332,7 +332,7 @@ type 'TY file =
     stdlib_syms : Sym.Set.t;
     mk_functions : function_to_convert list;
     resource_predicates : (Sym.t * Definition.Predicate.t) list;
-    logical_predicates : (Sym.t * Definition.Function.definition) list;
+    logical_predicates : (Sym.t * Definition.Function.t) list;
     datatypes : (Sym.t * datatype) list;
     lemmata : (Sym.t * (Locations.t * ArgumentTypes.lemmat)) list;
     call_funinfo : (Sym.t, Sctypes.c_concrete_sig) Pmap.map
diff --git a/backend/cn/lib/pack.ml b/backend/cn/lib/pack.ml
index fee01a4df..aeeb9da63 100644
--- a/backend/cn/lib/pack.ml
+++ b/backend/cn/lib/pack.ml
@@ -90,7 +90,7 @@ let packing_ft loc global provable ret =
        Some at
      | PName pn ->
        let def = Sym.Map.find pn global.resource_predicates in
-       (match identify_right_clause provable def ret.pointer ret.iargs with
+       (match Predicate.identify_right_clause provable def ret.pointer ret.iargs with
         | None -> None
         | Some right_clause -> Some right_clause.packing_ft))
   | Q _ -> None
diff --git a/backend/cn/lib/simplify.ml b/backend/cn/lib/simplify.ml
index a81d0c287..432f55f7d 100644
--- a/backend/cn/lib/simplify.ml
+++ b/backend/cn/lib/simplify.ml
@@ -597,7 +597,7 @@ module IndexTerms = struct
           t
         else (
           let def = Sym.Map.find name simp_ctxt.global.logical_functions in
-          match Definition.Function.try_open_fun def args with
+          match Definition.Function.try_open def args with
           | Some inlined -> aux inlined
           | None -> t)
       | _ ->
diff --git a/backend/cn/lib/solver.ml b/backend/cn/lib/solver.ml
index 79556766d..141293aae 100644
--- a/backend/cn/lib/solver.ml
+++ b/backend/cn/lib/solver.ml
@@ -1002,8 +1002,8 @@ let rec translate_term s iterm =
   | MapDef _ -> failwith "MapDef"
   | Apply (name, args) ->
     let def = Option.get (get_logical_function_def s.globals name) in
-    (match def.definition with
-     | Def body -> translate_term s (Definition.Function.open_fun def.args body args)
+    (match def.body with
+     | Def body -> translate_term s (Definition.Function.open_ def.args body args)
      | _ ->
        let do_arg arg = translate_base_type (IT.basetype arg) in
        let args_ts = List.map do_arg args in
diff --git a/backend/cn/lib/testGeneration/genOptimize.ml b/backend/cn/lib/testGeneration/genOptimize.ml
index 94b3829b0..9ddb9d988 100644
--- a/backend/cn/lib/testGeneration/genOptimize.ml
+++ b/backend/cn/lib/testGeneration/genOptimize.ml
@@ -764,11 +764,11 @@ module PartialEvaluation = struct
           eval_aux (divisible_ (addr, align) here)
       | Apply (fsym, its) ->
         (match List.assoc_opt Sym.equal fsym prog5.logical_predicates with
-         | Some { args; definition = Def it_body; _ }
-         | Some { args; definition = Rec_Def it_body; _ } ->
+         | Some { args; body = Def it_body; _ } | Some { args; body = Rec_Def it_body; _ }
+           ->
            return
            @@ IT.subst (IT.make_subst (List.combine (List.map fst args) its)) it_body
-         | Some { definition = Uninterp; _ } ->
+         | Some { body = Uninterp; _ } ->
            Error ("Function " ^ Sym.pp_string fsym ^ " is uninterpreted")
          | None -> Error ("Function " ^ Sym.pp_string fsym ^ " was not found"))
       | Let ((x, it_v), it_rest) ->
@@ -1018,9 +1018,9 @@ module PartialEvaluation = struct
            * substitution, diverging. As such, we force strict evaluation of recursive calls
            *)
           (match List.assoc_opt Sym.equal fsym prog5.logical_predicates with
-           | Some { definition = Def _; _ } -> f it
-           | Some { definition = Rec_Def _; _ } -> f ~mode:Strict it
-           | Some { definition = Uninterp; _ } | None -> it)
+           | Some { body = Def _; _ } -> f it
+           | Some { body = Rec_Def _; _ } -> f ~mode:Strict it
+           | Some { body = Uninterp; _ } | None -> it)
         | _ -> f it
       in
       IT.map_term_post aux it
diff --git a/backend/cn/lib/typing.mli b/backend/cn/lib/typing.mli
index 63d628ed4..b46997b96 100644
--- a/backend/cn/lib/typing.mli
+++ b/backend/cn/lib/typing.mli
@@ -118,7 +118,7 @@ val get_lemma : Locations.t -> Sym.t -> (Locations.t * Global.AT.lemmat) m
 
 val get_resource_predicate_def : Locations.t -> Sym.t -> Definition.Predicate.t m
 
-val get_logical_function_def : Locations.t -> Sym.t -> Definition.Function.definition m
+val get_logical_function_def : Locations.t -> Sym.t -> Definition.Function.t m
 
 val add_struct_decl : Sym.t -> Memory.struct_layout -> unit m
 
@@ -131,7 +131,7 @@ val add_lemma : Sym.t -> Locations.t * ArgumentTypes.lemmat -> unit m
 
 val add_resource_predicate : Sym.t -> Definition.Predicate.t -> unit m
 
-val add_logical_function : Sym.t -> Definition.Function.definition -> unit m
+val add_logical_function : Sym.t -> Definition.Function.t -> unit m
 
 val add_datatype : Sym.t -> BaseTypes.dt_info -> unit m
 
diff --git a/backend/cn/lib/wellTyped.ml b/backend/cn/lib/wellTyped.ml
index e49d08a1c..527f33f96 100644
--- a/backend/cn/lib/wellTyped.ml
+++ b/backend/cn/lib/wellTyped.ml
@@ -2299,9 +2299,7 @@ end
 module WLFD = struct
   open Definition.Function
 
-  let welltyped
-    ({ loc; args; return_bt; emit_coq; definition } : Definition.Function.definition)
-    =
+  let welltyped ({ loc; args; return_bt; emit_coq; body } : Definition.Function.t) =
     (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
     pure
       (let@ args =
@@ -2313,8 +2311,8 @@ module WLFD = struct
            args
        in
        let@ return_bt = WBT.is_bt loc return_bt in
-       let@ definition =
-         match definition with
+       let@ body =
+         match body with
          | Def body ->
            let@ body = WIT.check loc return_bt body in
            return (Def body)
@@ -2323,7 +2321,7 @@ module WLFD = struct
            return (Rec_Def body)
          | Uninterp -> return Uninterp
        in
-       return { loc; args; return_bt; emit_coq; definition })
+       return { loc; args; return_bt; emit_coq; body })
 end
 
 module WLemma = struct