diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp
index 26f19940ae..8bddf1f869 100644
--- a/src/library/noncomputable.cpp
+++ b/src/library/noncomputable.cpp
@@ -77,7 +77,8 @@ static bool is_noncomputable(old_type_checker & tc, noncomputable_ext const & ex
     if (d.is_meta()) {
         return false; /* ignore nontrusted definitions */
     } else if (d.is_axiom()) {
-        return !env.is_builtin(d.get_name()) && !tc.is_prop(d.get_type()) && !is_builtin_extra(d.get_name());
+        return !env.is_builtin(d.get_name()) && !tc.is_prop(d.get_type()) && !is_sort(d.get_type()) &&
+               !is_builtin_extra(d.get_name());
     } else {
         return false;
     }