diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 40c7060a5..9a13cec64 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -213,11 +213,18 @@ struct structure_cmd_fn {
             m_type = m_p.parse_expr();
             if (!is_sort(m_type))
                 throw parser_error("invalid 'structure', 'Type' expected", pos);
-            if (has_placeholder(m_type))
-                throw_explicit_universe(pos);
-            level l = sort_level(m_type);
-            if (m_env.impredicative() && !is_not_zero(l))
-                throw parser_error("invalid 'structure', the resultant universe level should not be zero for any universe parameter assignment", pos);
+            if (m_infer_result_universe) {
+                if (!is_placeholder(sort_level(m_type)))
+                    throw parser_error("invalid 'structure', resultant universe level is computed "
+                                       "automatically when universe level parameters are not provided", pos);
+            } else {
+                if (has_placeholder(m_type))
+                    throw_explicit_universe(pos);
+                level l = sort_level(m_type);
+                if (m_env.impredicative() && !is_not_zero(l))
+                    throw parser_error("invalid 'structure', the resultant universe level should not be zero "
+                                       "for any universe parameter assignment", pos);
+            }
         } else {
             if (!m_infer_result_universe)
                 throw_explicit_universe(pos);
diff --git a/tests/lean/run/record9.lean b/tests/lean/run/record9.lean
new file mode 100644
index 000000000..1fe1fa379
--- /dev/null
+++ b/tests/lean/run/record9.lean
@@ -0,0 +1,8 @@
+import logic
+
+constant fibrant : Type → Prop
+
+structure Fib : Type :=
+{type : Type} (pred : fibrant type)
+
+check Fib.mk