diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index 60edab1f4896af1b9df22eded4c3e41354960d6b..2ef2b54fd166c89eb290dc09c16367f893045c83 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -104,8 +104,8 @@ impl<'arena> Term<'arena> {
     }
 
     /// Infers the type of the term `t`, living in arena `arena`.
-    pub fn infer(self, arena: &mut Arena<'arena>) -> ResultTerm<'arena> {
-        self.get_type_or_try_init(|| match *self {
+    pub fn infer_raw(self, arena: &mut Arena<'arena>) -> ResultTerm<'arena> {
+        match *self {
             Sort(lvl) => Ok(Term::sort(lvl.succ(arena), arena)),
             Var(_, type_) => Ok(type_),
 
@@ -153,8 +153,13 @@ impl<'arena> Term<'arena> {
                 }
             },
 
-            Decl(decl) => decl.get_type_or_try_init(Term::infer, arena),
-        })
+            Decl(decl) => decl.get_type_or_try_init(Term::infer_raw, arena),
+        }
+    }
+
+    /// Infers the type of the term `t`, living in arena `arena`, checks for memoization.
+    pub fn infer(self, arena: &mut Arena<'arena>) -> ResultTerm<'arena> {
+        self.get_type_or_try_init(|| self.infer_raw(arena))
     }
 
     /// Checks whether the term `t` living in `arena` is of type `ty`.
@@ -222,6 +227,26 @@ mod tests {
         })
     }
 
+    #[test]
+    fn infer_decl() {
+        //use std::env;
+        //env::set_var("RUST_BACKTRACE", "1");
+        use_arena(|arena| {
+            let decl_ = crate::memory::declaration::InstantiatedDeclaration::instantiate(
+                crate::memory::declaration::builder::Builder::Decl(crate::memory::term::builder::Builder::Prop.into(), Vec::new())
+                    .realise(arena)
+                    .unwrap(),
+                &Vec::new(),
+                arena,
+            );
+
+            let term = crate::memory::term::Term::decl(decl_, arena);
+            let ty = arena.build_term_raw(type_usize(0));
+
+            assert!(term.check(ty, arena).is_ok());
+        })
+    }
+
     #[test]
     fn def_eq_2() {
         use_arena(|arena| {