# HG changeset patch
# User haftmann
# Date 1679682617 0
# Node ID 5af3954ed6cf3c746623c297ad7093d86d5e4883
# Parent  86b9a405b0cc3b2c08b6fb164f079666cef53ddd
tuned

diff -r 86b9a405b0cc -r 5af3954ed6cf 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';