# HG changeset patch
# User desharna
# Date 1641820403 -3600
# Node ID 70aab133dc8dbd4ce6227aa9ee84d2e5a56ecf00
# Parent  5d3a846bccf83678652cecb42c2322336325845c
proper abstraction of function variables when instantiating induction rules in Sledgehammer

diff -r 5d3a846bccf8 -r 70aab133dc8d src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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