be more open-minded and allow needless mutual recursion for 'prim(co)rec', since we allow it for '(co)datatype' -- eventual warnings (or errors) should be centralized in 'fp_bnf'
1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Wed Nov 06 13:00:45 2013 +0100
1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Wed Nov 06 14:50:50 2013 +0100
1.3 @@ -286,9 +286,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 nor nested recursive via " ^
1.9 - qsotys Ts2);
1.10
1.11 val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T);
1.12
1.13 @@ -302,9 +299,6 @@
1.14 if fp = fp' then
1.15 let
1.16 val mutual_Ts = map (fn Type (s, _) => Type (s, tyargs)) Ts';
1.17 - val _ =
1.18 - seen = [] orelse exists (exists_subtype_in seen) mutual_Ts orelse
1.19 - not_mutually_nested_rec mutual_Ts seen;
1.20 val (seen', Ts') = List.partition (member (op =) mutual_Ts) Ts;
1.21 in
1.22 mutual_Ts @ check_enrich_with_mutuals (seen @ T :: seen') Ts'