reverted check introduced in ce58fb149ff6, now that independent functions are allowed (cf. 347c3b0cab44)
1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Mon Nov 11 17:38:53 2013 +0100
1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Mon Nov 11 17:40:55 2013 +0100
1.3 @@ -284,9 +284,6 @@
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 @@ -319,9 +316,6 @@
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. *)