diff -r 35a1788dd6f9 -r dd222e2af01a src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Tue Apr 18 21:47:40 2023 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Tue Apr 18 22:24:48 2023 +0200
@@ -44,7 +44,7 @@
       Element.instantiate_normalize_morphism (TFrees.empty, param_map_inst);
     val typ_morph =
       Element.instantiate_normalize_morphism
-        (TFrees.make [(a_tfree, certT (Term.aT [class]))], Frees.empty)
+        (TFrees.make1 (a_tfree, certT (Term.aT [class])), Frees.empty)
     val (([raw_props], _, [(_, raw_inst_morph)], _, export_morph), _) = thy_ctxt
       |> Expression.cert_goal_expression ([(class, (("", false),
            (Expression.Named param_map_const, [])))], []);