# HG changeset patch
# User blanchet
# Date 1370420866 -7200
# Node ID 608afd26a476a0ef745a645bc2021db904666c38
# Parent  0215f48d9b6421765e5e5a02a515f4af3dda0968
killed dead code

diff -r 0215f48d9b64 -r 608afd26a476 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Jun 05 10:21:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Jun 05 10:27:46 2013 +0200
@@ -275,7 +275,6 @@
       | project T = T;
   in project end;
 
-val project_recT = project_co_recT @{type_name prod};
 val project_corecT = project_co_recT @{type_name sum};
 
 fun unzip_recT Cs (T as Type (@{type_name prod}, Ts as [_, U])) =
@@ -305,7 +304,6 @@
       map3 (fn n => fn ms => map2 (map (unzip_recT Cs) oo dest_tupleT) ms o
         dest_sumTN_balanced n o domain_type) ns mss ctor_rec_fun_Ts;
 
-    val z_Tsss = map3 mk_fun_arg_typess ns mss ctor_rec_fun_Ts;
     val z_Tsss' = map (map (flat_rec I)) z_Tssss;
     val h_Tss = map2 (map2 (curry (op --->))) z_Tsss' Css;
 
@@ -467,13 +465,8 @@
         | _ => build_simple TU);
   in build end;
 
-fun mk_iter_body lthy Cs ctor_iter fss xssss =
-  let
-    fun build_proj sel sel_const (x as Free (_, T)) =
-      build_map lthy (sel_const o fst) (T, project_recT Cs sel T) $ x;
-  in
-    Term.list_comb (ctor_iter, map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss)
-  end;
+fun mk_iter_body ctor_iter fss xssss =
+  Term.list_comb (ctor_iter, map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss);
 
 fun mk_preds_getterss_join c cps sum_prod_T cqfss =
   let val n = length cqfss in
@@ -509,7 +502,7 @@
         val binding = mk_binding suf;
         val spec =
           mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)),
-            mk_iter_body lthy0 Cs ctor_iter fss xssss);
+            mk_iter_body ctor_iter fss xssss);
       in (binding, spec) end;
 
     val binding_specs =
diff -r 0215f48d9b64 -r 608afd26a476 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Jun 05 10:21:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Jun 05 10:27:46 2013 +0200
@@ -113,7 +113,6 @@
     val s'Ts = map2 (fn T => fn U => T --> U) activeBs FTsBs;
     val s''Ts = map2 (fn T => fn U => T --> U) activeCs FTsCs;
     val fTs = map2 (fn T => fn U => T --> U) activeAs activeBs;
-    val all_fTs = map2 (fn T => fn U => T --> U) allAs allBs;
     val self_fTs = map (fn T => T --> T) activeAs;
     val gTs = map2 (fn T => fn U => T --> U) activeBs activeCs;
     val all_gTs = map2 (fn T => fn U => T --> U) allBs allCs';
@@ -154,11 +153,10 @@
     val hrecTs = map fastype_of Zeros;
     val hsetTs = map (fn hrecT => Library.foldr (op -->) (sTs, HOLogic.natT --> hrecT)) hrecTs;
 
-    val (((((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2),
+    val (((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2),
       z's), As), As_copy), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
-      self_fs), all_fs), gs), all_gs), xFs), xFs_copy), yFs), yFs_copy), RFs), (Rtuple, Rtuple')),
-      (hrecs, hrecs')), (nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), Kss),
-      names_lthy) = lthy
+      self_fs), gs), all_gs), xFs), yFs), yFs_copy), RFs), (Rtuple, Rtuple')), (hrecs, hrecs')),
+      (nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), Kss), names_lthy) = lthy
       |> mk_Frees' "b" activeAs
       ||>> mk_Frees "b" activeAs
       ||>> mk_Frees "b" activeAs
@@ -176,11 +174,9 @@
       ||>> mk_Frees "f" fTs
       ||>> mk_Frees "f" fTs
       ||>> mk_Frees "f" self_fTs
-      ||>> mk_Frees "f" all_fTs
       ||>> mk_Frees "g" gTs
       ||>> mk_Frees "g" all_gTs
       ||>> mk_Frees "x" FTsAs
-      ||>> mk_Frees "x" FTsAs
       ||>> mk_Frees "y" FTsBs
       ||>> mk_Frees "y" FTsBs
       ||>> mk_Frees "x" FRTs