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 =