# HG changeset patch
# User blanchet
# Date 1348140768 -7200
# Node ID 416ad6e2343b197b19fd1046742923e96d4364c5
# Parent  f1f2a03e866914494a908b5444335e5f64998ca7
tuning

diff -r f1f2a03e8669 -r 416ad6e2343b src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- 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 ();
diff -r f1f2a03e8669 -r 416ad6e2343b src/HOL/Codatatype/Tools/bnf_gfp.ML
--- 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;
diff -r f1f2a03e8669 -r 416ad6e2343b src/HOL/Codatatype/Tools/bnf_wrap.ML
--- 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;