diff --git a/library/standard/diaconescu.lean b/library/standard/diaconescu.lean
index cb39fa754e..730693fb6a 100644
--- a/library/standard/diaconescu.lean
+++ b/library/standard/diaconescu.lean
@@ -8,7 +8,7 @@ using eq_proofs
 -- Show that Excluded middle follows from
 --   Hilbert's choice operator, function extensionality and Prop extensionality
 section
-hypothesis propext ⦃a b : Prop⦄ : (a → b) → (b → a) → a = b
+hypothesis propext {a b : Prop} : (a → b) → (b → a) → a = b
 
 parameter p : Prop
 
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index b7a6e711d9..28ee51e916 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -258,6 +258,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
         type = Pi_as_is(section_ps, type, p);
         value = Fun_as_is(section_ps, value, p);
         levels section_ls = collect_section_levels(ls, p);
+        for (expr & p : section_ps)
+            p = mk_explicit(p);
         expr ref = mk_implicit(mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_ps));
         p.add_local_expr(n, ref);
     }