--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 20 11:42:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 20 13:32:48 2012 +0200
@@ -81,6 +81,7 @@
no_defs_lthy0 =
let
(* TODO: sanity checks on arguments *)
+ (* TODO: integration with function package ("size") *)
val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
else ();
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 20 11:42:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 20 13:32:48 2012 +0200
@@ -2266,9 +2266,8 @@
(tcoalg_thm RS bis_diag_thm))))
|> Thm.close_derivation;
- (*### FIXME: get rid of mem_Id_eq_eq? or Id_def'? *)
val pred_of_rel_thms =
- rel_defs @ @{thms Id_def' mem_Collect_eq fst_conv mem_Id_eq_eq snd_conv split_conv};
+ rel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv};
val pred_coinduct = unfold_defs lthy pred_of_rel_thms rel_coinduct;
val pred_coinduct_upto = unfold_defs lthy pred_of_rel_thms rel_coinduct_upto;
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Thu Sep 20 11:42:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Thu Sep 20 13:32:48 2012 +0200
@@ -82,9 +82,7 @@
(raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
let
(* TODO: sanity checks on arguments *)
- (* TODO: attributes (simp, case_names, etc.) *)
(* TODO: case syntax *)
- (* TODO: integration with function package ("size") *)
val n = length raw_ctrs;
val ks = 1 upto n;