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/Pure/axclass.ML
changeset 81512 c1aa8a61ee65
parent 81507 08574da77b4a 
--- a/src/Pure/axclass.ML	Sat Nov 30 13:40:57 2024 +0100
+++ b/src/Pure/axclass.ML	Sat Nov 30 13:41:38 2024 +0100
@@ -280,12 +280,12 @@
     val binding =
       Binding.concealed (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
 
-    val args = Name.invent_types_global Ss;
+    val args = map TFree (Name.invent_types_global Ss);
     val missing_params =
       Sign.complete_sort thy [c]
       |> maps (these o Option.map #params o try (get_info thy))
       |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
-      |> (map o apsnd o map_atyps) (K (Type (t, map TFree args)));
+      |> (map o apsnd o map_atyps) (K (Type (t, args)));
   in
     thy
     |> Global_Theory.store_thm (binding, th)
isabelle