diff --git a/tests/lean/trace1.lean b/tests/lean/trace1.lean
index 6a0853609e..4d18330160 100644
--- a/tests/lean/trace1.lean
+++ b/tests/lean/trace1.lean
@@ -5,15 +5,15 @@ namespace trace
 
 meta def test (opts : options) : id trace_map :=
 prod.snd <$> trace_t.run opts (
-trace_root ⟨1, 0⟩ `trace.type_context.is_def_eq "type_context.is_def_eq trace" (
-  trace_ctx `trace.type_context.is_def_eq "f 0 =?= f a (approximate mode)" (
-    trace_ctx `trace.type_context.is_def_eq_detail "f 0 =?= f a" (
+trace_root ⟨1, 0⟩ `trace.type_context.is_def_eq "type_context.is_def_eq trace" ⟨λ _,
+  trace_ctx `trace.type_context.is_def_eq "f 0 =?= f a (approximate mode)" ⟨λ _,
+    trace_ctx `trace.type_context.is_def_eq_detail "f 0 =?= f a" ⟨λ _,
       trace `trace.type_context.is_def_eq_detail "0 =?= a" >>
       trace `trace.type_context.is_def_eq_detail "...failed"
-    ) >>
+    ⟩ >>
     trace `trace.type_context.is_def_eq "...failed"
-  )
-))
+  ⟩
+⟩)
 
 run_cmd
 do let test opts := tactic.trace $ format.join $ list.intersperse format.line $ (test opts).to_list.map $ λ ⟨pos, tr⟩, to_fmt pos ++ ": " ++ tr.pp,