--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Nov 29 17:40:15 2024 +0100
@@ -72,7 +72,7 @@
fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
let
- val frees = map Free (Name.invent_names Name.context "a" (map (K \<^typ>\<open>narrowing_term\<close>) tys))
+ val frees = map Free (Name.invent_names_global "a" (map (K \<^typ>\<open>narrowing_term\<close>) tys))
val narrowing_term =
\<^term>\<open>Quickcheck_Narrowing.Narrowing_constructor\<close> $ HOLogic.mk_number \<^typ>\<open>integer\<close> i $
HOLogic.mk_list \<^typ>\<open>narrowing_term\<close> (rev frees)