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/quickcheck_common.ML
changeset 81519 cdc43c0fdbfc
parent 74561 8e6c973003c8 
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sat Nov 30 22:33:21 2024 +0100
@@ -248,7 +248,7 @@
           @{thm bot_fun_def}, @{thm less_bool_def}])
     val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term ctxt t)
     val (vs, body) = strip_all t'
-    val vs' = Variable.variant_frees ctxt [t'] vs
+    val vs' = Variable.variant_names (Variable.declare_names t' ctxt) vs
   in subst_bounds (map Free (rev vs'), body) end
isabelle