src/HOL/BNF/Tools/bnf_fp_util.ML

--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Fri Jun 07 08:57:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Fri Jun 07 09:28:59 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 un_fold_of: 'a list -> 'a
+  val co_rec_of: 'a list -> 'a
 
   val time: Timer.real_timer -> string -> Timer.real_timer
 
@@ -215,6 +217,9 @@
 fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
   eq_list eq_bnf (bnfs1, bnfs2);
 
+fun un_fold_of [f, _] = f;
+fun co_rec_of [_, r] = r;
+
 val timing = true;
 fun time timer msg = (if timing
   then warning (msg ^ ": " ^ ATP_Util.string_of_time (Timer.checkRealTimer timer))