# HG changeset patch
# User blanchet
# Date 1411566384 -7200
# Node ID e4e34dfc3e68d595f85be6463d0a568291046c50
# Parent  cc1bab5558b00497c49db7b54b8653324d1e51b8
rule out nested (co)recursion for SMT (co)datatypes

diff -r cc1bab5558b0 -r e4e34dfc3e68 src/HOL/Tools/SMT/smt_datatypes.ML
--- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 24 15:46:23 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 24 15:46:24 2014 +0200
@@ -71,8 +71,23 @@
       | info :: _ => (get_typedef_decl info T Ts, ctxt))
   in
     (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
-      SOME {fp = fp', ctr_sugar, ...} =>
-      if fp' = fp then get_ctr_sugar_decl ctr_sugar T Ts ctxt else ([], ctxt)
+      SOME {fp = fp', fp_res = {Ts = fp_Ts, ...}, ctr_sugar, ...} =>
+      if fp' = fp then
+        let
+          val ns = map (fst o dest_Type) fp_Ts
+          val mutual_fp_sugars = map_filter (BNF_FP_Def_Sugar.fp_sugar_of ctxt) ns
+          val Xs = map #X mutual_fp_sugars
+          val ctrXs_Tsss = map #ctrXs_Tss mutual_fp_sugars
+
+          fun is_nested_co_recursive (T as Type _) =
+              BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs T
+            | is_nested_co_recursive _ = false
+        in
+          if exists (exists (exists is_nested_co_recursive)) ctrXs_Tsss then maybe_typedef ()
+          else get_ctr_sugar_decl ctr_sugar T Ts ctxt
+        end
+      else
+        ([], ctxt)
     | NONE =>
       if fp = BNF_Util.Least_FP then
         if String.isSuffix extN n then