diff --git a/KLR/Util/Sexp.lean b/KLR/Util/Sexp.lean
index 759ef3c7..44826ea1 100644
--- a/KLR/Util/Sexp.lean
+++ b/KLR/Util/Sexp.lean
@@ -442,7 +442,8 @@ private def mkFromSexpBodyForStruct (indName : Name) : TermElabM Term := do
       let getter ← `(doElem| Except.mapError (fun s => (toString $(quote indName)) ++ "." ++ (toString $(quote field)) ++ ": " ++ s) <| $getter)
       return getter
   )
-  let fields := fields.map mkIdent
+  let fieldNames := fields.map mkIdent
+  let fieldValues <- fields.mapM fun f => return mkIdent (<- Lean.Core.mkFreshUserName f) --  mkIdent f.capitalize
   let name <- Meta.nameToStrLit indName
   `(do
       let n <- sexp.length?
@@ -453,11 +454,11 @@ private def mkFromSexpBodyForStruct (indName : Name) : TermElabM Term := do
         | some k => throw s!"No field named {k} in {$name}"
         | none => pure ()
       try
-        $[let $fields:ident ← $getNamed]*
-        return { $[$fields:ident := $(id fields)],* }
+        $[let $fieldValues:ident ← $getNamed]*
+        return { $[$fieldNames:ident := $(fieldValues)],* }
       catch _ =>
-        $[let $fields:ident ← $getPositional]*
-        return { $[$fields:ident := $(id fields)],* }
+        $[let $fieldValues:ident ← $getPositional]*
+        return { $[$fieldNames:ident := $(fieldValues)],* }
   )
 
 /-
diff --git a/KLR/Util/SexpTest.lean b/KLR/Util/SexpTest.lean
index e423ed7c..f7d99207 100644
--- a/KLR/Util/SexpTest.lean
+++ b/KLR/Util/SexpTest.lean
@@ -179,3 +179,19 @@ private structure Default6 where
 deriving BEq, FromSexp, Repr
 
 #guard @fromSexp? Default6 _ (sexp%()) == .ok (Default6.mk)
+
+structure pseudo_core_barrier where
+  id : UInt32
+  semaphore : UInt32
+deriving FromSexp
+
+-- Was broken in earlier version. It generated
+--    assocWithDefault✝ _ sexp✝ "arg" (id { })
+-- but id was not the identity function, but the projection
+private structure IdArg where
+deriving FromSexp
+
+private structure Id where
+  id : Nat
+  arg : IdArg := {}
+deriving FromSexp