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/Library/refute.ML
changeset 81541 5335b1ca6233
parent 81516 31b05aef022d 
--- a/src/HOL/Library/refute.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/HOL/Library/refute.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -1186,7 +1186,7 @@
           (a, T) :: strip_all_vars t
       | strip_all_vars _ = [] : (string * typ) list
     val strip_t = strip_all_body ex_closure
-    val frees = Term.variant_frees strip_t (strip_all_vars ex_closure)
+    val frees = Term.variant_bounds strip_t (strip_all_vars ex_closure)
     val subst_t = Term.subst_bounds (map Free (rev frees), strip_t)
   in
     find_model ctxt (actual_params ctxt params) assm_ts subst_t true
isabelle