Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
changeset 81519 cdc43c0fdbfc
parent 71394 933ad2385480 
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Sat Nov 30 22:33:21 2024 +0100
@@ -279,14 +279,12 @@
                 let
                   val (constr, args) = strip_comb t
                   val T = fastype_of t
+                  val ctxt1 = fold Variable.declare_names (concl :: assms) ctxt
                   val vars =
-                    map Free
-                      (Variable.variant_frees ctxt (concl :: assms)
-                        (map (fn t => ("x", fastype_of t)) args))
+                    map Free (Variable.variant_names ctxt1 (map (fn t => ("x", fastype_of t)) args))
                   val varnames = map (fst o dest_Free) vars
-                  val dummy_var =
-                    Free (singleton
-                      (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T))
+                  val ctxt2 = fold Variable.declare_names vars ctxt1
+                  val dummy_var = Free (singleton (Variable.variant_names ctxt2) ("dummy", T))
                   val new_assms = map HOLogic.mk_eq (vars ~~ args)
                   val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars)
                   val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine
isabelle