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/Data_Structures/Define_Time_Function.ML
changeset 81519 cdc43c0fdbfc
parent 81358 91b008474f1b
child 82081 50dd4fc40fcb 
--- a/src/HOL/Data_Structures/Define_Time_Function.ML	Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML	Sat Nov 30 22:33:21 2024 +0100
@@ -883,7 +883,7 @@
             | args _ = []
           val dom_vars =
             terms |> hd |> get_l |> map_types (map_atyps freeTypes)
-            |> args |> Variable.variant_frees lthy []
+            |> args |> Variable.variant_names lthy
           val dom_args = 
             List.foldl (fn (t,p) => HOLogic.mk_prod ((Free t),p)) (Free (hd dom_vars)) (tl dom_vars)
isabelle