proper abstraction of function variables when instantiating induction rules in Sledgehammer

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jan 10 13:11:18 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jan 10 14:13:23 2022 +0100
@@ -392,7 +392,7 @@
 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
   let
     fun varify_noninducts (t as Free (s, T)) =
-        if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
+        if (s, T) = ind_x then t else Var ((s, 0), T)
       | varify_noninducts t = t
 
     val p_inst = concl_prop