diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean
index 4e3d2d01c0..3b61289b90 100644
--- a/src/Init/Lean/Meta/ExprDefEq.lean
+++ b/src/Init/Lean/Meta/ExprDefEq.lean
@@ -999,5 +999,7 @@ partial def isExprDefEqAuxImpl : Expr → Expr → MetaM Bool
 @[init] def setIsExprDefEqAuxRef : IO Unit :=
 isExprDefEqAuxRef.set isExprDefEqAuxImpl
 
+abbrev isDefEq := @isExprDefEq
+
 end Meta
 end Lean
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 3641be1c20..fd31eef6c0 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -177,8 +177,8 @@ do print "----- tst6 -----";
      m2 ← mkFreshExprMVar type;
      let t := mkApp io x;
      -- we need to use foApprox to solve `?m1 ?m2 =?= IO x`
-     check $ not <$> isExprDefEq (mkApp m1 m2) t;
-     check $ approxDefEq $ isExprDefEq (mkApp m1 m2) t;
+     check $ not <$> isDefEq (mkApp m1 m2) t;
+     check $ approxDefEq $ isDefEq (mkApp m1 m2) t;
      v ← getAssignment m1;
      check $ pure $ v == io;
      v ← getAssignment m2;