# HG changeset patch
# User blanchet
# Date 1473593727 -7200
# Node ID 6f74e9aea81672a2fa6b13145b8472c2448de919
# Parent  fdf90aa5986835d5062f5983cff40b0e13b313c2
tuning

diff -r fdf90aa59868 -r 6f74e9aea816 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Sep 11 13:35:27 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Sep 11 13:35:27 2016 +0200
@@ -983,20 +983,19 @@
                   apfst flat (fold_map (fn set => fn ctxt =>
                     let
                       val T = HOLogic.dest_setT (range_type (fastype_of set));
-                      val (x, ctxt') = yield_singleton (mk_Frees "x") T ctxt;
-                      val assm = mk_Trueprop_mem (x, set $ t);
+                      val (y, ctxt') = yield_singleton (mk_Frees "y") T ctxt;
+                      val assm = mk_Trueprop_mem (y, set $ t);
                     in
-                      apfst (map (Logic.mk_implies o pair assm)) (mk_goals A setA ctr_args x ctxt')
+                      apfst (map (Logic.mk_implies o pair assm)) (mk_goals A setA ctr_args y ctxt')
                     end) (map (mk_set innerTs) (sets_of_bnf bnf)) ctxt))
               | T => (if T = A then [mk_Trueprop_mem (t, setA $ ctr_args)] else [], ctxt));
 
             val (goalssss, _) =
               fold_map (fn set =>
                 let val A = HOLogic.dest_setT (range_type (fastype_of set)) in
-                  fold_map (fn ctr => fn ctxt =>
-                    let val (args, ctxt') = mk_Frees "a" (binder_types (fastype_of ctr)) ctxt in
-                      fold_map (mk_goals A set (Term.list_comb (ctr, args))) args ctxt'
-                    end) ctrAs
+                  @{fold_map 2} (fn ctr => fn xs =>
+                      fold_map (mk_goals A set (Term.list_comb (ctr, xs))) xs)
+                    ctrAs xss
                 end) setAs lthy;
             val goals = flat (flat (flat goalssss));
           in