diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index c811a5bc33..0fa392dda2 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -82,7 +82,6 @@ structure Config :=
 structure ParamInfo :=
 (implicit     : Bool      := false)
 (instImplicit : Bool      := false)
-(proof        : Bool      := false)
 (hasFwdDeps   : Bool      := false)
 (backDeps     : Array Nat := #[])
 
diff --git a/src/Init/Lean/Meta/FunInfo.lean b/src/Init/Lean/Meta/FunInfo.lean
index ae297a6d6e..089f571d1d 100644
--- a/src/Init/Lean/Meta/FunInfo.lean
+++ b/src/Init/Lean/Meta/FunInfo.lean
@@ -62,12 +62,10 @@ checkFunInfoCache fn maxArgs? $ do
         (fun (i : Nat) (pinfo : Array ParamInfo) => do
           let fvar := fvars.get! i;
           decl ← getFVarLocalDecl fvar;
-          proof ← isProp decl.type;
           let backDeps := collectDeps fvars decl.type;
           let pinfo    := updateHasFwdDeps pinfo backDeps;
           pure $ pinfo.push {
             backDeps     := backDeps,
-            proof        := proof,
             implicit     := decl.binderInfo == BinderInfo.implicit,
             instImplicit := decl.binderInfo == BinderInfo.instImplicit })
         #[];