src/Pure/Isar/specification.ML
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 *)