reintroduce mutually (co)rec check, since the underlying N2M code doesn't quite handle the general case (esp. in presence of type variables)
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Thu Nov 07 01:01:04 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Thu Nov 07 02:42:20 2013 +0100
@@ -284,6 +284,9 @@
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);
@@ -316,6 +319,9 @@
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. *)