fix: remove kabstractWithPred

The function `kabstractWithPred` was never used, and introduced the
bug exposed by issue #1235.

fixes #1235

src/Lean/Meta/KAbstract.lean

@@ -41,35 +41,4 @@ def kabstract (e : Expr) (p : Expr) (occs : Occurrences := Occurrences.all) : Me
         visitChildren ()
     visit e 0 |>.run' 1
 
-/--
-  Similar to `kabstract`, but only abstracts occurrences of `p` s.t. `pred parent? p` is true where `parent?`
-  is the parent expression for `p` if any.
--/
-partial def kabstractWithPred (e : Expr) (p : Expr) (pred : (parent? : Option Expr) → (e : Expr) → MetaM Bool) : MetaM Expr := do
-  let e ← instantiateMVars e
-  let pHeadIdx := p.toHeadIndex
-  let pNumArgs := p.headNumArgs
-  let rec visit (parent? : Option Expr) (e : Expr) (offset : Nat) : MetaM Expr := do
-    let visitChildren : Unit → MetaM Expr := fun _ => do
-      match e with
-      | Expr.app ..          => e.withApp fun f args => return mkAppN (← visit e f offset) (← args.mapM (visit e . offset))
-      | Expr.mdata _ b _     => return e.updateMData! (← visit e b offset)
-      | Expr.proj _ _ b _    => return e.updateProj! (← visit e b offset)
-      | Expr.letE _ t v b _  => return e.updateLet! (← visit e t offset) (← visit e v offset) (← visit e b (offset+1))
-      | Expr.lam _ d b _     => return e.updateLambdaE! (← visit e d offset) (← visit e b (offset+1))
-      | Expr.forallE _ d b _ => return e.updateForallE! (← visit e d offset) (← visit e b (offset+1))
-      | e                    => return e
-    if e.hasLooseBVars then
-      visitChildren ()
-    else if e.toHeadIndex != pHeadIdx || e.headNumArgs != pNumArgs then
-      visitChildren ()
-    else if (← isDefEq e p) then
-      if (← pred parent? e) then
-        return mkBVar offset
-      else
-        visitChildren ()
-    else
-      visitChildren ()
-  visit none e 0
-
 end Lean.Meta

src/Lean/Meta/Tactic/Generalize.lean

@@ -18,7 +18,7 @@ structure GeneralizeArg where
 
 partial def generalize
     (mvarId : MVarId) (args : Array GeneralizeArg)
-    (pred : (parent? : Option Expr) → (e : Expr) → MetaM Bool := fun _ _ => return true)
+    -- (pred : (parent? : Option Expr) → (e : Expr) → MetaM Bool := fun _ _ => return true)
     : MetaM (Array FVarId × MVarId) :=
   withMVarContext mvarId do
     checkNotAssigned mvarId `generalize
@@ -31,7 +31,7 @@ partial def generalize
         let eType ← instantiateMVars (← inferType e)
         let type ← go (i+1)
         let xName ← if let some xName := arg.xName? then pure xName else mkFreshUserName `x
-        return Lean.mkForall xName BinderInfo.default eType (← kabstractWithPred type e pred)
+        return Lean.mkForall xName BinderInfo.default eType (← kabstract type e)
       else
         return target
     let targetNew ← go 0

tests/lean/1235.lean

@@ -0,0 +1,8 @@
+opaque f (a b : Nat) : Nat
+example : f 1 2 = f 2 1 := by
+  generalize h : f 1 = g
+  /- g : ℕ → ℕ
+  h : f 1 = g
+  ⊢ g 2 = f 2 1 -/
+  trace_state
+  sorry

tests/lean/1235.lean.expected.out

@@ -0,0 +1,4 @@
+1235.lean:2:0-2:7: warning: declaration uses 'sorry'
+g : Nat → Nat
+h : f 1 = g
+⊢ g 2 = f 2 1