# HG changeset patch
# User blanchet
# Date 1367936322 -7200
# Node ID ba735ac9044ae3c254bf9a219527bb7ad09028cb
# Parent  126f8d11f87354caae64dfdb2226525585a44327
removed dead code

diff -r 126f8d11f873 -r ba735ac9044a src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 16:15:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 16:18:42 2013 +0200
@@ -26,7 +26,6 @@
 
   val exists_subtype_in: typ list -> typ -> bool
   val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c
-  val mk_fp_iter: bool -> typ list -> typ list -> term list -> term list * typ list
   val mk_un_fold_co_rec_prelims: bool -> typ list -> typ list -> typ list -> int list ->
     int list list -> term list -> term list -> Proof.context ->
     (term list * term list * ((term list list * typ list list * term list list list)
@@ -41,10 +40,6 @@
 
   val mk_iter_fun_arg_types_pairsss: typ list -> int list -> int list list -> term ->
     (typ list * typ list) list list list
-  val mk_folds_recs: Proof.context -> typ list -> typ list -> typ list -> int list ->
-    int list list -> term list -> term list -> term list * term list
-  val mk_unfolds_corecs: Proof.context -> typ list -> typ list -> typ list -> int list ->
-    int list list -> term list -> term list -> term list * term list
   val define_fold_rec: (term list list * typ list list * term list list list)
       * (term list list * typ list list * term list list list) -> (string -> binding) -> typ list ->
     typ list -> typ list -> term -> term -> Proof.context ->
@@ -438,22 +433,6 @@
     Term.list_comb (ctor_iter, map2 (mk_sum_caseN_balanced oo map2 mk_iter_arg) fss xsss)
   end;
 
-fun mk_folds_recs lthy fpTs As Cs ns mss ctor_folds ctor_recs =
-  let
-    val (_, ctor_fold_fun_Ts) = mk_fp_iter true As Cs ctor_folds;
-    val (_, ctor_rec_fun_Ts) = mk_fp_iter true As Cs ctor_recs;
-
-    val (((gss, _, ysss), (hss, _, zsss)), _) =
-      mk_fold_rec_args_types fpTs Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy;
-
-    fun mk_term ctor_iter fss xsss =
-      fold_rev (fold_rev Term.lambda) fss (mk_iter_body lthy fpTs ctor_iter fss xsss);
-
-    fun mk_terms ctor_fold ctor_rec = (mk_term ctor_fold gss ysss, mk_term ctor_rec hss zsss);
-  in
-    map2 mk_terms ctor_folds ctor_recs |> split_list
-  end;
-
 fun mk_preds_getterss_join c cps sum_prod_T cqfss =
   let val n = length cqfss in
     Term.lambda c (mk_IfN sum_prod_T cps
@@ -474,24 +453,6 @@
     Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss)
   end;
 
-fun mk_unfolds_corecs lthy fpTs As Cs ns mss dtor_unfolds dtor_corecs =
-  let
-    val (_, dtor_unfold_fun_Ts) = mk_fp_iter true As Cs dtor_unfolds;
-    val (_, dtor_corec_fun_Ts) = mk_fp_iter true As Cs dtor_corecs;
-
-    val ((cs, cpss, unfold_only, corec_only), _) =
-      mk_unfold_corec_args_types fpTs Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts lthy;
-
-    fun mk_term dtor_coiter ((pfss, cqssss, cfssss), (f_sum_prod_Ts, f_Tsss, _)) =
-      fold_rev (fold_rev Term.lambda) pfss
-        (mk_coiter_body lthy cs cpss f_sum_prod_Ts f_Tsss cqssss cfssss dtor_coiter);
-
-    fun mk_terms dtor_unfold dtor_corec =
-      (mk_term dtor_unfold unfold_only, mk_term dtor_corec corec_only);
-  in
-    map2 mk_terms dtor_unfolds dtor_corecs |> split_list
-  end;
-
 fun define_fold_rec (fold_only, rec_only) mk_binding fpTs As Cs ctor_fold ctor_rec no_defs_lthy =
   let
     val nn = length fpTs;