diff -r 6a33337eb08d -r 94bace5078ba src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Sun Oct 20 22:40:18 2024 +0200 +++ b/src/Pure/Isar/specification.ML Mon Oct 21 11:55:51 2024 +0200 @@ -94,7 +94,7 @@ fun get Cs (Const ("_type_constraint_", C) $ t) = get (C :: Cs) t | get Cs (Free (y, T)) = if x = y then - map_filter Term_Position.decode_positionT + maps Term_Position.decode_positionT (T :: map (Type.constraint_type ctxt) Cs) else [] | get _ (t $ u) = get [] t @ get [] u