# HG changeset patch
# User blanchet
# Date 1384188055 -3600
# Node ID bd36da55d8256dbd437908e55cfbcccf199c3ce3
# Parent  bc24e1ccfd35c7b7c46b8366070ee00e5c7d930e
reverted check introduced in ce58fb149ff6, now that independent functions are allowed (cf. 347c3b0cab44)

diff -r bc24e1ccfd35 -r bd36da55d825 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 11 17:38:53 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 11 17:40:55 2013 +0100
@@ -284,9 +284,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 " ^ qsotys Ts2 ^
-        " nor nested recursive via " ^ qsotys Ts2);
 
     val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T);
 
@@ -319,9 +316,6 @@
           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. *)