src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 55968 94242fa87638
parent 55966 972f0aa7091b
child 56049 c6a15aa64e36
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Mar 07 12:35:06 2014 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Mar 07 14:21:15 2014 +0100
@@ -478,8 +478,8 @@
       define_co_rec Least_FP fpT Cs (mk_binding recN)
         (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec,
            map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
-               mk_case_absumprod ctor_rec_absT rep fs
-                 (map (mk_tuple_balanced o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss))
+               mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss)
+                 (map flat_rec_arg_args xsss))
              ctor_rec_absTs reps fss xssss)))
     end;