tuning
authorblanchet
Wed, 29 May 2013 02:35:49 +0200
changeset 52213 f4c5c6320cce
parent 52212 afe61eefdc61
child 52214 4cc5a80bba80
tuning
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;