1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 11 18:13:17 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 11 18:25:13 2013 +0100
     1.3 @@ -283,6 +283,9 @@
     1.4          else
     1.5            not_co_datatype0 T
     1.6        | not_co_datatype T = not_co_datatype0 T;
     1.7 +    fun not_mutually_nested_rec Ts1 Ts2 =
     1.8 +      error (qsotys Ts1 ^ " is neither mutually recursive with " ^ qsotys Ts2 ^
     1.9 +        " nor nested recursive via " ^ qsotys Ts2);
    1.10  
    1.11      val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T);
    1.12  
    1.13 @@ -315,6 +318,9 @@
    1.14            val {fp_res = {Ts = mutual_Ts0, ...}, ...} = the_fp_sugar_of T;
    1.15            val mutual_Ts = map (retypargs tyargs) mutual_Ts0;
    1.16  
    1.17 +          val _ = seen = [] orelse exists (exists_subtype_in seen) mutual_Ts orelse
    1.18 +            not_mutually_nested_rec mutual_Ts seen;
    1.19 +
    1.20            fun fresh_tyargs () =
    1.21              let
    1.22                (* The name "'z" is unlikely to clash with the context, yielding more cache hits. *)