# HG changeset patch
# User nipkow
# Date 1731833454 -3600
# Node ID bb82ebb18b5dc3384ee72a5881cd07e57802b213
# Parent  42b0f923fd82ae27fe96882f523c2119fa8a8ed2
Use Var to maintain the difference between function and locale parameters

diff -r 42b0f923fd82 -r bb82ebb18b5d src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sat Nov 16 22:46:33 2024 +0100
+++ b/src/HOL/Tools/Function/function.ML	Sun Nov 17 09:50:54 2024 +0100
@@ -76,10 +76,9 @@
     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)
+    fun varify (ps,prop) =
+      Term.subst_bounds (rev (map (fn (a,T) => Var((a,0),T)) ps), Term.strip_all_body prop)
+    val input_eqns = map varify (map Term.strip_all_vars props0 ~~ props0)
     val fnames = map (fst o fst) fixes0
     val defname = Binding.conglomerate fnames;