diff --git a/tests/compiler/termparsertest1.lean b/tests/compiler/termparsertest1.lean
index 5a4b29770b..222ce942ac 100644
--- a/tests/compiler/termparsertest1.lean
+++ b/tests/compiler/termparsertest1.lean
@@ -57,7 +57,7 @@ test [
 "{ x // p x 10 }",
 "{ x : Nat // p x 10 }",
 "{ .. }",
-"{ Prod . fst := 10, .. }",
+"{ fst := 10, .. : Nat × Nat }",
 "a[i]",
 "f [10, 20]",
 "g a[x+2]",
diff --git a/tests/compiler/termparsertest1.lean.expected.out b/tests/compiler/termparsertest1.lean.expected.out
index 1d5e7f1f23..28bd42815f 100644
--- a/tests/compiler/termparsertest1.lean.expected.out
+++ b/tests/compiler/termparsertest1.lean.expected.out
@@ -138,6 +138,8 @@ fun (Prod.mk x y) => f y x
   (Term.structInstField `x (null) ":=" (Term.num (numLit "10")))
   ","
   (Term.structInstField `y (null) ":=" (Term.num (numLit "20"))))
+ (null)
+ (null)
  "}")
 { x := 10, y := 20, }
 (Term.structInst
@@ -148,6 +150,8 @@ fun (Prod.mk x y) => f y x
   ","
   (Term.structInstField `y (null) ":=" (Term.num (numLit "20")))
   ",")
+ (null)
+ (null)
  "}")
 { x // p x 10 }
 (Term.subtype "{" `x (null) "//" (Term.app (Term.id `p (null)) (null (Term.id `x (null)) (Term.num (numLit "10")))) "}")
@@ -160,12 +164,14 @@ fun (Prod.mk x y) => f y x
  (Term.app (Term.id `p (null)) (null (Term.id `x (null)) (Term.num (numLit "10"))))
  "}")
 { .. }
-(Term.structInst "{" (null) (null (Term.structInstSource ".." (null))) "}")
-{ Prod . fst := 10, .. }
+(Term.structInst "{" (null) (null) (null "..") (null) "}")
+{ fst := 10, .. : Nat × Nat }
 (Term.structInst
  "{"
- (null `Prod ".")
- (null (Term.structInstField `fst (null) ":=" (Term.num (numLit "10"))) "," (Term.structInstSource ".." (null)))
+ (null)
+ (null (Term.structInstField `fst (null) ":=" (Term.num (numLit "10"))) ",")
+ (null "..")
+ (null ":" (Term.prod (Term.id `Nat (null)) "×" (Term.id `Nat (null))))
  "}")
 a[i]
 (Term.arrayRef (Term.id `a (null)) "[" (Term.id `i (null)) "]")
@@ -382,7 +388,9 @@ let { fst := x, .. } := f 10; x + x
   (Term.structInst
    "{"
    (null)
-   (null (Term.structInstField `fst (null) ":=" (Term.id `x (null))) "," (Term.structInstSource ".." (null)))
+   (null (Term.structInstField `fst (null) ":=" (Term.id `x (null))) ",")
+   (null "..")
+   (null)
    "}")
   (null)
   (null)
diff --git a/tests/lean/run/structInst.lean b/tests/lean/run/structInst.lean
index be33fdd452..0770411461 100644
--- a/tests/lean/run/structInst.lean
+++ b/tests/lean/run/structInst.lean
@@ -51,31 +51,31 @@ new_frontend
 
 namespace Ex1
 
-#check { B . y := 1 }
-#check { C . z := 1 }
+#check { y := 1 : B }
+#check { z := 1 : C }
 
 end Ex1
 
 namespace Ex2
 
-#check { B . x := 1 }
+#check { x := 1 : B }
 
 end Ex2
 
 namespace Ex3
 
-#check { C . x := 1 }
-#check { C . y := 1 }
-#check { C . z := 1 }
+#check { x := 1 : C }
+#check { y := 1 : C }
+#check { z := 1 : C }
 
 end Ex3
 
 namespace Ex4
 
-#check { C . x := 1 } -- works
-#check { C . y := 1 } -- works
-#check { C . z := 1 } -- works
-#check { C . z := 1, x := 2 } -- works
-#check { B . y := 1 } -- works
+#check { x := 1 : C } -- works
+#check { y := 1 : C } -- works
+#check { z := 1 : C } -- works
+#check { z := 1, x := 2 : C } -- works
+#check { y := 1 : B } -- works
 
 end Ex4
diff --git a/tests/lean/run/structInst3.lean b/tests/lean/run/structInst3.lean
index ab7fd33295..a54ab755d1 100644
--- a/tests/lean/run/structInst3.lean
+++ b/tests/lean/run/structInst3.lean
@@ -18,10 +18,10 @@ open Ex1
 
 def c1 : C Nat := { x := 1 }
 
-#check { z := 2, .. c1 }
+#check { c1 with z := 2 }
 
 def c2 : C (Nat × Nat) := { z := (1, 1) }
 
-#check { x.fst := 2, .. c2 }
+#check { c2 with x.fst := 2 }
 
-#check { x.1 := 3, .. c2 }
+#check { c2 with x.1 := 3 }
diff --git a/tests/lean/run/structInst4.lean b/tests/lean/run/structInst4.lean
index a1b7ad5958..a0eefded0c 100644
--- a/tests/lean/run/structInst4.lean
+++ b/tests/lean/run/structInst4.lean
@@ -11,17 +11,17 @@ new_frontend
 
 #check (b).modifyOp (idx := 1) (fun s => 2)
 
-#check { [1] := 2, .. b }
+#check { b with [1] := 2 }
 
-#check { [1].fst.2 := 1, .. a }
+#check { a with [1].fst.2 := 1 }
 
 def foo : Foo := {}
 
 #check foo.x[1].1.2
 
-#check { x[1].2 := true, .. foo }
-#check { x[1].fst.snd := 1, .. foo }
-#check { x[1].1.fst := 1, .. foo }
+#check { foo with x[1].2 := true }
+#check { foo with x[1].fst.snd := 1 }
+#check { foo with x[1].1.fst := 1 }
 
-#check { x[1].1.1 := 5, .. foo }
-#check { x[1].1.2 := 5, .. foo }
+#check { foo with x[1].1.1 := 5 }
+#check { foo with x[1].1.2 := 5 }