--- 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, [])))], []);