diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean
index c67012a95d..fed44282d7 100644
--- a/src/Lean/Meta/Tactic/Cbv/Main.lean
+++ b/src/Lean/Meta/Tactic/Cbv/Main.lean
@@ -135,7 +135,7 @@ def simplifyAppFn : Simproc := fun e => do
       return .rfl
     else
     let res ← simp fn
-    match (← simp fn) with
+    match res with
     | .rfl _ => return res
     | .step e' proof _ =>
       let newType ← Sym.inferType e'
diff --git a/tests/lean/run/cbv1.lean b/tests/lean/run/cbv1.lean
index f2af066280..af76b3cab6 100644
--- a/tests/lean/run/cbv1.lean
+++ b/tests/lean/run/cbv1.lean
@@ -176,8 +176,8 @@ attribute [cbv_opaque] Std.DHashMap.emptyWithCapacity
 attribute [cbv_opaque] Std.DHashMap.insert
 attribute [cbv_opaque] Std.DHashMap.getEntry
 attribute [cbv_opaque] Std.DHashMap.contains
-attribute [cbv_eval Std.DHashMap.contains] Std.DHashMap.contains_emptyWithCapacity
-attribute [cbv_eval Std.DHashMap.contains] Std.DHashMap.contains_insert
+attribute [cbv_eval] Std.DHashMap.contains_emptyWithCapacity
+attribute [cbv_eval] Std.DHashMap.contains_insert
 
 example : ((Std.DHashMap.emptyWithCapacity : Std.DHashMap Nat (fun _ => Nat)).insert 5 3).contains 5 = true := by
   conv =>