--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 03 12:48:20 2014 +0100
@@ -30,8 +30,6 @@
rel_xtor_co_induct_thm: thm}
val morph_fp_result: morphism -> fp_result -> fp_result
- val un_fold_of: 'a list -> 'a
- val co_rec_of: 'a list -> 'a
val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer
@@ -236,11 +234,6 @@
xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm};
-fun un_fold_of [f, _] = f;
-
-fun co_rec_of [r] = r
- | co_rec_of [_, r] = r;
-
fun time ctxt timer msg = (if Config.get ctxt bnf_timing
then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
"ms")