# HG changeset patch
# User blanchet
# Date 1369787749 -7200
# Node ID f4c5c6320cce73a175156643210a4db0c11e4720
# Parent  afe61eefdc61cebf2c791ceca5a47c07579aa0c4
tuning

diff -r afe61eefdc61 -r f4c5c6320cce src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 28 23:11:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed May 29 02:35:49 2013 +0200
@@ -309,7 +309,7 @@
         val f_Tsss = map2 (map2 dest_tupleT o repair_arity) mss f_prod_Tss;
         val f_Tssss = map2 (fn C => map (map (map (curry (op -->) C) o maybe_unzipT))) Cs f_Tsss;
         val q_Tssss =
-          map (map (map (fn [_] => [] | [_, C] => [mk_pred1T (domain_type C)]))) f_Tssss;
+          map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss;
         val pf_Tss = map3 flat_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
       in (q_Tssss, f_Tssss, (f_sum_prod_Ts, f_Tsss, pf_Tss)) end;