# HG changeset patch
# User blanchet
# Date 1347213440 -7200
# Node ID f9fc2b64c59991544935f8c6c9da08785043f53f
# Parent  4626ff7cbd2ce647c0797934fd37e6516384ca0d
fixed bug with one-value codatatype "codata 'a dead_foo = A"

diff -r 4626ff7cbd2c -r f9fc2b64c599 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 19:05:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 19:57:20 2012 +0200
@@ -535,10 +535,10 @@
           let
             fun mk_goal_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not);
 
-            fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr cfs' =
+            fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr m cfs' =
               fold_rev (fold_rev Logic.all) ([c] :: pfss)
                 (Logic.list_implies (seq_conds mk_goal_cond n k cps,
-                   mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, cfs'))));
+                   mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, take m cfs'))));
 
             fun build_call fiter_likes maybe_tack (T, U) =
               if T = U then
@@ -558,13 +558,13 @@
               else
                 cf;
 
-            val cgsss = map (map (map (repair_calls gcoiters (K I) (K I)))) cgsss;
-            val chsss = map (map (map (repair_calls hcorecs (curry mk_sumT) (tack z)))) chsss;
+            val cgsss' = map (map (map (repair_calls gcoiters (K I) (K I)))) cgsss;
+            val chsss' = map (map (map (repair_calls hcorecs (curry mk_sumT) (tack z)))) chsss;
 
             val goal_coiterss =
-              map7 (map3 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss cgsss;
+              map8 (map4 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss mss cgsss';
             val goal_corecss =
-              map7 (map3 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss chsss;
+              map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss chsss';
 
             val coiter_tacss =
               map3 (map oo mk_coiter_like_tac coiter_defs map_ids) fp_iter_thms pre_map_defs
diff -r 4626ff7cbd2c -r f9fc2b64c599 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 09 19:05:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 09 19:57:20 2012 +0200
@@ -65,6 +65,7 @@
   Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN
   subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
   Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN
-  Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1;
+  Local_Defs.unfold_tac ctxt @{thms id_def} THEN
+  (rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1;
 
 end;