changeset 80632 | 3a196e63a80d |
parent 78469 | 53b59fa42696 |
child 80635 | 27d5452d20fc |
--- a/src/Pure/Isar/specification.ML Sat Aug 03 13:12:58 2024 +0200 +++ b/src/Pure/Isar/specification.ML Sun Aug 04 12:21:13 2024 +0200 @@ -324,7 +324,7 @@ val type_alias = gen_alias Local_Theory.type_alias (K (K (fn c => (c, [])))); val type_alias_cmd = - gen_alias Local_Theory.type_alias (apfst (#1 o dest_Type) ooo Proof_Context.check_type_name); + gen_alias Local_Theory.type_alias (apfst dest_Type_name ooo Proof_Context.check_type_name); (* fact statements *)