--- a/src/Doc/Datatypes/Datatypes.thy Thu Aug 29 07:49:54 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Aug 29 08:05:29 2013 +0200
@@ -1123,6 +1123,11 @@
* no direct way to define recursive functions for default values -- but show trick
based on overloading
+
+* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
+ (for datatype\_compat and prim(co)rec)
+
+* no way to register same type as both data- and codatatype?
*}
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 07:49:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 08:05:29 2013 +0200
@@ -149,6 +149,8 @@
fun co_induct_of (i :: _) = i;
fun strong_co_induct_of [_, s] = s;
+(* TODO: register "sum" and "prod" as datatypes to enable N2M reduction for them *)
+
fun register_fp_sugar key fp_sugar =
Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));