tuned
authorhaftmann
Fri, 24 Mar 2023 18:30:17 +0000
changeset 77701 5af3954ed6cf
parent 77700 86b9a405b0cc
child 77702 b5fbe9837aee
tuned
src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Tools/Code/code_thingol.ML	Fri Mar 24 18:30:17 2023 +0000
@@ -638,7 +638,7 @@
     val class_params = these_class_params class;
     val superclass_params = maps these_class_params
       ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
-    val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
+    val vs = Name.invent_names Name.context Name.aT (Sorts.mg_domain algebra tyco [class]);
     val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
     val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
       Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';