src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML

     fun generalize_type T (seen_lthy as (seen, _)) =
       (case AList.lookup (op =) seen T of
         SOME U => (U, seen_lthy)
       | NONE =>
         (case T of
-          Type (s, Ts) =>
-          if exists_subtype_in Ts T then fold_map generalize_type Ts seen_lthy |>> curry Type s
+          Type (s, Ts') =>
+          if exists_subtype_in Ts T then fold_map generalize_type Ts' seen_lthy |>> curry Type s
           else generalize_simple_type T seen_lthy
         | _ => generalize_simple_type T seen_lthy));
 
     val (perm_Us, _) = fold_map generalize_type perm_Ts ([], lthy);