diff --git a/library/Init/Lean/Meta/Default.lean b/library/Init/Lean/Meta/Default.lean
index 9707322ea2..57b0b6c9ad 100644
--- a/library/Init/Lean/Meta/Default.lean
+++ b/library/Init/Lean/Meta/Default.lean
@@ -37,9 +37,9 @@ private partial def auxFixpoint : MetaOp → Expr → Expr → MetaM Expr
   let synthPending := fun e => pure false;     -- TODO
   match op with
   | whnfOp         => whnfAux inferType isDefEq synthPending e₁
-  | inferTypeOp    => inferType e₁
-  | synthPendingOp => boolToExpr <$> synthPending e₁
-  | isDefEqOp      => boolToExpr <$> isDefEq e₁ e₂
+  | inferTypeOp    => inferTypeAux whnf e₁
+  | synthPendingOp => boolToExpr <$> pure false
+  | isDefEqOp      => boolToExpr <$> pure false
 
 def whnf (e : Expr) : MetaM Expr :=
 auxFixpoint whnfOp e e