diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
index 73eadf0ed..0901fe39d 100644
--- a/src/sail_lean_backend/pretty_print_lean.ml
+++ b/src/sail_lean_backend/pretty_print_lean.ml
@@ -284,7 +284,7 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) =
       nest 2 (flow (break 1) [string "let"; string id; coloneq; doc_exp ctxt lexp]) ^^ hardline ^^ doc_exp ctxt e
   | E_struct fexps ->
       let args = List.map (doc_fexp ctxt) fexps in
-      braces (separate comma args)
+      braces (separate (comma ^^ space) args)
   | E_field (exp, id) -> doc_exp ctxt exp ^^ dot ^^ doc_id_ctor id
   | E_struct_update (exp, fexps) ->
       let args = List.map (doc_fexp ctxt) fexps in
diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
index dff53c3d9..4157dbdd7 100644
--- a/test/lean/struct.expected.lean
+++ b/test/lean/struct.expected.lean
@@ -14,6 +14,10 @@ def struct_field2 (s : My_struct) : (BitVec 1) :=
 def struct_update_field2 (s : My_struct) (b : (BitVec 1)) : My_struct :=
   {s with field2 := b}
 
+/-- Type quantifiers: i : Int -/
+def mk_struct (i : Int) (b : (BitVec 1)) : My_struct :=
+  {field1 := i, field2 := b}
+
 def initialize_registers : Unit :=
   ()
 
diff --git a/test/lean/struct.sail b/test/lean/struct.sail
index 5a3fc670e..4d249a4ee 100644
--- a/test/lean/struct.sail
+++ b/test/lean/struct.sail
@@ -15,4 +15,12 @@ function struct_field2(s) = {
 val struct_update_field2 : (My_struct, bit) -> My_struct
 function struct_update_field2(s, b) = {
   { s with field2 = b }
+}
+
+val mk_struct : (int, bit) -> My_struct
+function mk_struct(i, b) = {
+  struct { 
+    field1 = i,
+    field2 = b
+  }
 }
\ No newline at end of file