src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML

            is_some (Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then
           error (qsoty T ^ " is not a new-style datatype (cf. \"datatype_new\")")
         else
           not_co_datatype0 T
       | not_co_datatype T = not_co_datatype0 T;
+    fun not_mutually_nested_rec Ts1 Ts2 =
+      error (qsotys Ts1 ^ " is neither mutually recursive with " ^ qsotys Ts2 ^
+        " nor nested recursive via " ^ qsotys Ts2);
 
     val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T);
 
     val perm_actual_Ts =
       sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts;

     fun gather_types _ _ num_groups seen gen_seen [] = (num_groups, seen, gen_seen)
       | gather_types lthy rho num_groups seen gen_seen ((T as Type (_, tyargs)) :: Ts) =
         let
           val {fp_res = {Ts = mutual_Ts0, ...}, ...} = the_fp_sugar_of T;
           val mutual_Ts = map (retypargs tyargs) mutual_Ts0;
+
+          val _ = seen = [] orelse exists (exists_subtype_in seen) mutual_Ts orelse
+            not_mutually_nested_rec mutual_Ts seen;
 
           fun fresh_tyargs () =
             let
               (* The name "'z" is unlikely to clash with the context, yielding more cache hits. *)
               val (gen_tyargs, lthy') =