| changeset 80632 | 3a196e63a80d |
| parent 80329 | d90a96894644 |
| child 80739 | 60801e5fae26 |
--- a/src/Pure/Isar/proof_context.ML Sat Aug 03 13:12:58 2024 +0200 +++ b/src/Pure/Isar/proof_context.ML Sun Aug 04 12:21:13 2024 +0200 @@ -608,7 +608,7 @@ in val read_arity = - prep_arity ((#1 o dest_Type) oo read_type_name {proper = true, strict = true}) Syntax.read_sort; + prep_arity (dest_Type_name oo read_type_name {proper = true, strict = true}) Syntax.read_sort; val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);