--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Fri Jun 07 11:42:37 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Fri Jun 07 12:00:29 2013 +0200
@@ -28,6 +28,8 @@
val morph_fp_result: morphism -> fp_result -> fp_result
val eq_fp_result: fp_result * fp_result -> bool
+ val weak_co_induct_of: 'a list -> 'a
+ val strong_co_induct_of: 'a list -> 'a
val un_fold_of: 'a list -> 'a
val co_rec_of: 'a list -> 'a
@@ -217,6 +219,9 @@
fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
eq_list eq_bnf (bnfs1, bnfs2);
+fun weak_co_induct_of [w, _] = w;
+fun strong_co_induct_of [_, s] = s;
+
fun un_fold_of [f, _] = f;
fun co_rec_of [_, r] = r;