# HG changeset patch
# User blanchet
# Date 1383745850 -3600
# Node ID 23c0049e7c409e342cc3f720cbde73ff9fef7302
# Parent  3ffb74b52ed6ad03727af4bcc1fe6a4d5e6a5f05
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'

diff -r 3ffb74b52ed6 -r 23c0049e7c40 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Nov 06 13:00:45 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Nov 06 14:50:50 2013 +0100
@@ -286,9 +286,6 @@
         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 nor nested recursive via " ^
-        qsotys Ts2);
 
     val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T);
 
@@ -302,9 +299,6 @@
           if fp = fp' then
             let
               val mutual_Ts = map (fn Type (s, _) => Type (s, tyargs)) Ts';
-              val _ =
-                seen = [] orelse exists (exists_subtype_in seen) mutual_Ts orelse
-                not_mutually_nested_rec mutual_Ts seen;
               val (seen', Ts') = List.partition (member (op =) mutual_Ts) Ts;
             in
               mutual_Ts @ check_enrich_with_mutuals (seen @ T :: seen') Ts'