src/HOL/Tools/BNF/bnf_lfp_size.ML

             SOME f => f
           | NONE => if member (op =) Cs T then Term.absdummy T (Bound 0) else mk_abs_zero_nat T)
       | mk_size_of_typ (T as Type (s, Ts)) =
         if is_pair_C s Ts then
           pair (snd_const T)
-        else if exists (exists_subtype_in As) Ts then
+        else if exists (exists_subtype_in (As @ Cs)) Ts then
           (case Symtab.lookup data s of
             SOME (size_name, (_, size_o_maps as _ :: _)) =>
             let
               val (args, size_o_mapss') = split_list (map (fn T => mk_size_of_typ T []) Ts);
               val size_const = Const (size_name, map fastype_of args ---> mk_to_natT T);