diff -r 07c802837a8c -r 29e60ca6ec01 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Nov 08 22:52:29 2024 +0100
+++ b/src/HOL/Tools/Function/function.ML	Wed Nov 13 23:10:58 2024 +0100
@@ -75,7 +75,11 @@
     val fixes = map (apfst (apfst Binding.name_of)) fixes0
     val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0
     val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
-
+    val props0 = map snd spec0
+    val vars0 = map Term.strip_all_vars props0
+    val input_eqns =
+      map (fn (ps,prop) => Term.subst_bounds (rev (map Free ps), Term.strip_all_body prop))
+        (vars0 ~~ props0)
     val fnames = map (fst o fst) fixes0
     val defname = Binding.conglomerate fnames;
 
@@ -122,7 +126,7 @@
           { add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps',
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', totality=NONE,
           fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases',
-          pelims=pelims',elims=NONE}
+          pelims=pelims', elims=NONE, input_eqns = input_eqns}
 
         val _ =
           Proof_Display.print_consts do_print (Position.thread_data ()) lthy2
@@ -180,7 +184,7 @@
           | NONE => error "Not a function"))
 
     val { termination, fs, R, add_simps, case_names, psimps,
-      pinducts, defname, fnames, cases, dom, pelims, ...} = info
+      pinducts, defname, fnames, cases, dom, pelims, input_eqns, ...} = info
     val domT = domain_type (fastype_of R)
     val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
     fun afterqed [[raw_totality]] lthy1 =
@@ -204,7 +208,7 @@
           let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps,
             case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,
             simps=SOME simps, inducts=SOME inducts, termination=termination, totality=SOME totality,
-            cases=cases, pelims=pelims, elims=SOME elims}
+            cases=cases, pelims=pelims, elims=SOME elims, input_eqns = input_eqns}
             |> transform_function_data (Morphism.binding_morphism "" prep_binding)
           in
             (info',