diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index df70464ef..0d1e62e9e 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -101,7 +101,7 @@ struct level_param_core : public level_cell {
     }
 };
 
-bool is_param_core(level const & l) { return is_param(l) || is_meta(l); }
+bool is_param_core(level const & l) { return is_param(l) || is_global(l) || is_meta(l); }
 
 static level_param_core const & to_param_core(level const & l) {
     lean_assert(is_param_core(l));