# HG changeset patch
# User blanchet
# Date 1410948573 -7200
# Node ID cdce4471d5906789c40aa4ef4c4c2e8dbcf9e814
# Parent  a416218a3a11b3c5fdab985522193d1a42d8bfea
tweaked compatibility layer

diff -r a416218a3a11 -r cdce4471d590 src/HOL/Datatype_Examples/Compat.thy
--- a/src/HOL/Datatype_Examples/Compat.thy	Wed Sep 17 11:54:59 2014 +0200
+++ b/src/HOL/Datatype_Examples/Compat.thy	Wed Sep 17 12:09:33 2014 +0200
@@ -41,11 +41,11 @@
 
 datatype 'b w = W | W' "'b w \<times> 'b list"
 
-(* no support for sums of products:
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name w} *}
+
 datatype_compat w
-*)
 
-ML {* get_descrs @{theory} (0, 1, 1) @{type_name w} *}
+ML {* get_descrs @{theory} (2, 2, 1) @{type_name w} *}
 
 datatype ('c, 'b) s = L 'c | R 'b
 
diff -r a416218a3a11 -r cdce4471d590 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Sep 17 11:54:59 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Sep 17 12:09:33 2014 +0200
@@ -332,8 +332,15 @@
   end;
 
 fun infos_of_new_datatype_mutual_cluster lthy prefs fpT_name =
-  #5 (mk_infos_of_mutually_recursive_new_datatypes prefs subset [fpT_name] lthy)
-  handle ERROR _ => [];
+  let
+    fun get prefs =
+      #5 (mk_infos_of_mutually_recursive_new_datatypes prefs subset [fpT_name] lthy)
+      handle ERROR _ => [];
+  in
+    (case get prefs of
+      [] => if member (op =) prefs Keep_Nesting then [] else get (Keep_Nesting :: prefs)
+    | infos => infos)
+  end;
 
 fun get_all thy prefs =
   let