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/Build/export_theory.ML
changeset 81512 c1aa8a61ee65
parent 81507 08574da77b4a 
--- a/src/Pure/Build/export_theory.ML	Sat Nov 30 13:40:57 2024 +0100
+++ b/src/Pure/Build/export_theory.ML	Sat Nov 30 13:41:38 2024 +0100
@@ -263,7 +263,7 @@
         val args' = args |> filter (is_free o #1);
         val typargs' = typargs |> filter (is_free o #1);
         val used_typargs = fold (Name.declare o #1) typargs' used;
-        val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
+        val sorts = Name.invent_types used_typargs extra_shyps;
       in ((sorts @ typargs', args', prop), proof) end;
 
     fun standard_prop_of thm =
isabelle