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/Predicate_Compile/predicate_compile_aux.ML
changeset 81519 cdc43c0fdbfc
parent 80636 4041e7c8059d 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Nov 30 22:33:21 2024 +0100
@@ -1204,7 +1204,7 @@
 fun define_quickcheck_predicate t thy =
   let
     val (vs, t') = strip_abs t
-    val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs (* FIXME proper context!? *)
+    val vs' = Variable.variant_names (Proof_Context.init_global thy) vs (* FIXME proper context!? *)
     val t'' = subst_bounds (map Free (rev vs'), t')
     val (prems, concl) = strip_horn t''
     val constname = "quickcheck"
isabelle