diff --git a/.stainless-version b/.stainless-version
index c66cd4c1..70bca09b 100644
--- a/.stainless-version
+++ b/.stainless-version
@@ -1 +1 @@
-noxt-0.8.0-8-gf15f5b5
+noxt-0.8.1
diff --git a/stainless_extraction/src/expr/spec.rs b/stainless_extraction/src/expr/spec.rs
index aba6abd7..848599a7 100644
--- a/stainless_extraction/src/expr/spec.rs
+++ b/stainless_extraction/src/expr/spec.rs
@@ -116,7 +116,7 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
     // extraction to directly translate them to the surrounding function's
     // variables, instead of extracting new, unrelated identifiers.
 
-    let def_id = self.tcx().hir().local_def_id(hir_id).to_def_id();
+    let def_id = self.base.hir_to_def_id(hir_id);
     let outer_fn_txtcx = &self.txtcx;
     let outer_fn_params = self.dcx.params();
     let f = self.factory();
diff --git a/stainless_extraction/src/fns.rs b/stainless_extraction/src/fns.rs
index 6a702ee4..0060f054 100644
--- a/stainless_extraction/src/fns.rs
+++ b/stainless_extraction/src/fns.rs
@@ -1,6 +1,7 @@
 use super::*;
 
 use rustc_hir::def_id::DefId;
+use rustc_middle::ty::FnSig;
 
 use stainless_data::ast as st;
 
@@ -25,6 +26,8 @@ impl<'a> FnItem<'a> {
   }
 }
 
+/// This does not include the tparams as they are contained in the generics.
+#[derive(Clone, Debug)]
 pub struct FnSignature<'l> {
   pub id: &'l st::SymbolIdentifier<'l>,
   pub tparams: Vec<&'l st::TypeParameterDef<'l>>,
@@ -32,6 +35,19 @@ pub struct FnSignature<'l> {
   pub return_tpe: st::Type<'l>,
 }
 
+impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
+  /// Panics if the given HirId does not own a HIR body.
+  pub(super) fn hir_body(&self, hir_id: HirId) -> &'tcx hir::Body<'tcx> {
+    let body_id = self.tcx.hir().body_owned_by(hir_id);
+    self.tcx.hir().body(body_id)
+  }
+
+  pub(super) fn ty_fn_sig(&self, def_id: DefId) -> FnSig<'tcx> {
+    let poly_fn_sig = self.tcx.fn_sig(def_id);
+    self.tcx.liberate_late_bound_regions(def_id, poly_fn_sig)
+  }
+}
+
 /// Identifies the specific implementation/instance of a type class that is
 /// needed at a method call site.
 #[derive(Debug, Eq, PartialEq)]
@@ -49,10 +65,6 @@ pub struct TypeClassKey<'l> {
 impl PartialEq<st::ClassType<'_>> for TypeClassKey<'_> {
   fn eq(&self, other: &st::ClassType<'_>) -> bool {
     let st::ClassType { id, tps } = other;
-    let key = TypeClassKey {
-      id: *id,
-      recv_tps: tps.clone(),
-    };
-    key == *self
+    self.id == *id && self.recv_tps == *tps
   }
 }
diff --git a/stainless_extraction/src/krate.rs b/stainless_extraction/src/krate.rs
index a8a069ed..5f1a5fc2 100644
--- a/stainless_extraction/src/krate.rs
+++ b/stainless_extraction/src/krate.rs
@@ -23,7 +23,7 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
 
     impl<'xtor, 'l, 'tcx> ItemLikeVisitor<'tcx> for ItemVisitor<'xtor, 'l, 'tcx> {
       fn visit_item(&mut self, item: &'tcx hir::Item<'tcx>) {
-        let def_id = self.xtor.tcx.hir().local_def_id(item.hir_id()).to_def_id();
+        let def_id = self.xtor.hir_to_def_id(item.hir_id());
         let def_path_str = self.xtor.tcx.def_path_str(def_id);
 
         match &item.kind {
@@ -120,7 +120,7 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
         let fns = items
           .filter_map(|(hir_id, kind, defaultness)| match kind {
             AssocItemKind::Fn { .. } => {
-              let fn_id = self.xtor.tcx.hir().local_def_id(hir_id).to_def_id();
+              let fn_id = self.xtor.hir_to_def_id(hir_id);
               Some(self.xtor.create_fn_item(fn_id, !defaultness.has_value()))
             }
             // ignore consts and type aliases in impl blocks
@@ -316,8 +316,7 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
 
     // Extract the function signature
     let Generics { tparams, txtcx, .. } = self.get_or_extract_generics(def_id);
-    let poly_fn_sig = self.tcx.fn_sig(def_id);
-    let fn_sig = self.tcx.liberate_late_bound_regions(def_id, poly_fn_sig);
+    let fn_sig = self.ty_fn_sig(def_id);
     let params: Params<'l> = fn_sig
       .inputs()
       .iter()
@@ -349,12 +348,9 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
   /// Extract a local function
   pub(super) fn extract_local_fn(&mut self, fn_item: &FnItem<'l>) -> &'l st::FunDef<'l> {
     let f = self.factory();
-    let tcx = self.tcx;
 
     assert!(fn_item.def_id.is_local());
-    let hir_id = tcx
-      .hir()
-      .local_def_id_to_hir_id(fn_item.def_id.expect_local());
+    let hir_id = self.ldef_to_hir_id(fn_item.def_id.expect_local());
     let class_def = self.get_class_of_method(fn_item.fd_id);
 
     // Extract flags
@@ -483,10 +479,9 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
     let adt_def = self.tcx.adt_def(def_id);
 
     // Extract flags for local def ids.
-    let (flags, mut flags_by_symbol, hir_id_opt) = def_id
-      .as_local()
-      .map(|local_def_id| {
-        let hir_id = self.tcx.hir().local_def_id_to_hir_id(local_def_id);
+    let (flags, mut flags_by_symbol, hir_id_opt) = self
+      .def_to_hir_id(def_id)
+      .map(|hir_id| {
         let (carrier_flags, by_symbol) = self.extract_flags(hir_id);
         (carrier_flags.to_stainless(f), by_symbol, Some(hir_id))
       })
diff --git a/stainless_extraction/src/lib.rs b/stainless_extraction/src/lib.rs
index e39649f6..189ebeac 100644
--- a/stainless_extraction/src/lib.rs
+++ b/stainless_extraction/src/lib.rs
@@ -303,6 +303,20 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
     self.factory().Variable(new_id, var.tpe, flags)
   }
 
+  fn hir_to_def_id(&self, hir_id: HirId) -> DefId {
+    self.tcx.hir().local_def_id(hir_id).to_def_id()
+  }
+
+  /// Returns None if the `def_id` is not local.
+  fn ldef_to_hir_id(&self, ldi: LocalDefId) -> HirId {
+    self.tcx.hir().local_def_id_to_hir_id(ldi)
+  }
+
+  /// Returns None if the `def_id` is not local.
+  fn def_to_hir_id(&self, def_id: DefId) -> Option<HirId> {
+    def_id.as_local().map(|ldi| self.ldef_to_hir_id(ldi))
+  }
+
   /// Get a BodyExtractor for some item with a body (like a function)
   fn enter_body<T, F>(
     &mut self,
@@ -365,10 +379,7 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
     let local_def_id = tcx.hir().local_def_id(hir_id);
     assert!(tcx.has_typeck_results(local_def_id));
     let tables = tcx.typeck(local_def_id);
-
-    // Fetch the body and the corresponding DefContext containing all bindings
-    let body_id = tcx.hir().body_owned_by(hir_id);
-    let body = tcx.hir().body(body_id);
+    let body = base.hir_body(hir_id);
 
     BodyExtractor {
       arena,
@@ -400,16 +411,10 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
   }
 
   fn return_tpe(&mut self) -> st::Type<'l> {
-    let hir_id = self
-      .tcx()
-      .hir()
-      .local_def_id_to_hir_id(self.tables.hir_owner);
-    let sigs = self.tables.liberated_fn_sigs();
-    let sig = sigs.get(hir_id).unwrap();
-    let decl = self.tcx().hir().fn_decl_by_hir_id(hir_id).unwrap();
-    self
-      .base
-      .extract_ty(sig.output(), &self.txtcx, decl.output.span())
+    let hir_id = self.base.ldef_to_hir_id(self.tables.hir_owner);
+    let span = self.tcx().hir().span(hir_id);
+    let sig = self.base.ty_fn_sig(self.tables.hir_owner.to_def_id());
+    self.base.extract_ty(sig.output(), &self.txtcx, span)
   }
 
   fn extract_body_expr(&mut self, ldi: LocalDefId) -> st::Expr<'l> {