diff --git a/flake.lock b/flake.lock
index 90f072c..9c98579 100644
--- a/flake.lock
+++ b/flake.lock
@@ -11,11 +11,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1732881390,
-        "narHash": "sha256-BHsHEnl6S5YXU1UMHR/wryH1CNvNaN/kxg43VwOsWFc=",
+        "lastModified": 1733493308,
+        "narHash": "sha256-E1pqGoFWvOx01fD3uEKf1ynpGD78tmgkb1NtdL+kkSA=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "1172606b471b5d9913f95cfbf944d3b943736667",
+        "rev": "17583e1d57e487a2a90740b85b9fe55c41bead59",
         "type": "github"
       },
       "original": {
@@ -173,11 +173,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1732847586,
-        "narHash": "sha256-SnHHSBNZ+aj8mRzYxb6yXBl9ei3K3j5agC/D8Vjw/no=",
+        "lastModified": 1733452419,
+        "narHash": "sha256-eh2i2GtqdWVOP7yjiWtB8FMUWktCZ4vjo81n6g5mSiE=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "97210ddff72fe139815f4c1ac5da74b5b0dde2d7",
+        "rev": "020701e6057992329a7cfafc6e3c5d5658bbcf79",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index ff060cd..2243c14 100644
--- a/flake.nix
+++ b/flake.nix
@@ -98,6 +98,7 @@
 
         inputsFrom = [
           self.packages.${system}.default
+          charon-ml
         ];
       };
     });
diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml
index eca5577..95a6634 100644
--- a/lib/AstOfLlbc.ml
+++ b/lib/AstOfLlbc.ml
@@ -369,7 +369,9 @@ let rec typ_of_ty (env : env) (ty : Charon.Types.ty) : K.typ =
       (* Appears in some trait methods, so let's try to handle that. *)
       K.TBuf (typ_of_ty env t, false)
   | TTraitType _ -> failwith ("TODO: TraitTypes " ^ Charon.PrintTypes.ty_to_string env.format_env ty)
-  | TArrow (_, ts, t) -> Krml.Helpers.fold_arrow (List.map (typ_of_ty env) ts) (typ_of_ty env t)
+  | TArrow binder ->
+      let ts, t = binder.binder_value in
+      Krml.Helpers.fold_arrow (List.map (typ_of_ty env) ts) (typ_of_ty env t)
 
 and maybe_cg_array env t cg =
   match cg with