# HG changeset patch
# User blanchet
# Date 1393847300 -3600
# Node ID 3be27c07e36d2291203176e36907bc24b5afecea
# Parent  516ab2906e7e421a245737b6bd255f13d8a4b515
rationalized internals

diff -r 516ab2906e7e -r 3be27c07e36d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -352,12 +352,6 @@
     val y_Tsss = map5 (fn absT => fn repT => fn n => fn ms =>
         dest_absumprodT absT repT n ms o domain_type)
       absTs repTs ns mss (map un_fold_of ctor_iter_fun_Tss);
-    val g_Tss = map2 (fn C => map (fn y_Ts => y_Ts ---> C)) Cs y_Tsss;
-
-    val ((gss, ysss), lthy) =
-      lthy
-      |> mk_Freess "f" g_Tss
-      ||>> mk_Freesss "x" y_Tsss;
 
     val z_Tssss =
       map6 (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_iter_fun_Ts =>
@@ -368,12 +362,11 @@
     val z_Tsss' = map (map flat_rec_arg_args) z_Tssss;
     val h_Tss = map2 (map2 (curry (op --->))) z_Tsss' Css;
 
-    val hss = map2 (map2 retype_free) h_Tss gss;
-    val zssss_hd = map2 (map2 (map2 (retype_free o hd))) z_Tssss ysss;
-    val (zssss_tl, lthy) =
+    val (((hss, ysss), zssss), lthy) =
       lthy
-      |> mk_Freessss "y" (map (map (map tl)) z_Tssss);
-    val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl;
+      |> mk_Freess "f" h_Tss
+      ||>> mk_Freesss "x" (*###*)y_Tsss
+      ||>> mk_Freessss "y" z_Tssss;
   in
     ((h_Tss, z_Tssss, hss, zssss), lthy)
   end;