# HG changeset patch
# User blanchet
# Date 1347188697 -7200
# Node ID 43d2df3135595c5991938799cfc96d2ef08ed247
# Parent  0e551c2d5d8be78b1d67848f479f8440ae819d93
generate "fld_unf_corecs" as well

diff -r 0e551c2d5d8b -r 43d2df313559 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sun Sep 09 12:51:17 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sun Sep 09 13:04:57 2012 +0200
@@ -22,7 +22,6 @@
   val corecN: string
   val exhaustN: string
   val fldN: string
-  val fld_unf_coitersN: string
   val fld_exhaustN: string
   val fld_induct2N: string
   val fld_inductN: string
@@ -32,6 +31,8 @@
   val fld_recN: string
   val fld_recsN: string
   val fld_unfN: string
+  val fld_unf_coitersN: string
+  val fld_unf_corecsN: string
   val hsetN: string
   val hset_recN: string
   val inductN: string
@@ -166,6 +167,7 @@
 val fld_recsN = fld_recN ^ "s"
 val unf_corecN = unfN ^ "_" ^ corecN
 val unf_corecsN = unf_corecN ^ "s"
+val fld_unf_corecsN = fldN ^ "_" ^ unf_corecN ^ "s"
 
 val fld_unfN = fldN ^ "_" ^ unfN
 val unf_fldN = unfN ^ "_" ^ fldN
diff -r 0e551c2d5d8b -r 43d2df313559 src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sun Sep 09 12:51:17 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sun Sep 09 13:04:57 2012 +0200
@@ -2121,9 +2121,10 @@
     val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms;
     val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms;
 
-    val fld_coiter_thms = map3 (fn unf_inject => fn coiter => fn unf_fld =>
-      iffD1 OF [unf_inject, trans OF [coiter, unf_fld RS sym]])
-      unf_inject_thms coiter_thms unf_fld_thms;
+    fun mk_fld_unf_coiter_like_thm unf_inject unf_fld coiter =
+      iffD1 OF [unf_inject, trans OF [coiter, unf_fld RS sym]];
+
+    val fld_coiter_thms = map3 mk_fld_unf_coiter_like_thm unf_inject_thms unf_fld_thms coiter_thms;
 
     val timer = time (timer "fld definitions & thms");
 
@@ -2189,6 +2190,8 @@
         goals coiter_thms map_congs
       end;
 
+    val fld_corec_thms = map3 mk_fld_unf_coiter_like_thm unf_inject_thms unf_fld_thms corec_thms;
+
     val timer = time (timer "corec definitions & thms");
 
     val (unf_coinduct_thm, coinduct_params, rel_coinduct_thm, pred_coinduct_thm,
@@ -2989,7 +2992,8 @@
         (unf_exhaustN, unf_exhaust_thms),
         (fld_injectN, fld_inject_thms),
         (fld_exhaustN, fld_exhaust_thms),
-        (fld_unf_coitersN, fld_coiter_thms)]
+        (fld_unf_coitersN, fld_coiter_thms),
+        (fld_unf_corecsN, fld_corec_thms)]
         |> map (apsnd (map single))
         |> maps (fn (thmN, thmss) =>
           map2 (fn b => fn thms =>
@@ -2997,7 +3001,7 @@
           bs thmss)
   in
     ((unfs, flds, coiters, corecs, unf_fld_thms, fld_unf_thms, fld_inject_thms, fld_coiter_thms,
-      corec_thms (* FIXME: should be "fld_corec_thms" *)),
+      fld_corec_thms),
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;