--- 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
--- 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