# HG changeset patch
# User blanchet
# Date 1392795272 -3600
# Node ID 4a940ebceef8997d936b2eb65203776d86c3dd85
# Parent  6a1cbddebf86181cc5a96eda4bd92ddb3593521e
rewrote a small portion of code to avoid dependency on low-level constant

diff -r 6a1cbddebf86 -r 4a940ebceef8 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Feb 19 08:33:59 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Feb 19 08:34:32 2014 +0100
@@ -11,7 +11,8 @@
   type basic_lfp_sugar =
     {T: typ,
      fp_res_index: int,
-     ctor_recT: typ,
+     C: typ,
+     fun_arg_Tsss : typ list list list,
      ctr_defs: thm list,
      ctr_sugar: Ctr_Sugar.ctr_sugar,
      recx: term,
@@ -44,10 +45,9 @@
 struct
 
 open Ctr_Sugar
+open Ctr_Sugar_General_Tactics
 open BNF_Util
-open BNF_Tactics
 open BNF_FP_Util
-open BNF_FP_Def_Sugar
 open BNF_FP_Rec_Sugar_Util
 
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
@@ -81,7 +81,8 @@
 type basic_lfp_sugar =
   {T: typ,
    fp_res_index: int,
-   ctor_recT: typ,
+   C: typ,
+   fun_arg_Tsss : typ list list list,
    ctr_defs: thm list,
    ctr_sugar: ctr_sugar,
    recx: term,
@@ -133,22 +134,16 @@
     val perm_indices = map #fp_res_index perm_basic_lfp_sugars;
 
     val perm_ctrss = map (#ctrs o #ctr_sugar) perm_basic_lfp_sugars;
-    val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
 
     val nn0 = length arg_Ts;
     val nn = length perm_ctrss;
     val kks = 0 upto nn - 1;
 
-    val perm_ns = map length perm_ctr_Tsss;
-    val perm_mss = map (map length) perm_ctr_Tsss;
     val perm_ctr_offsets = map (fn kk => Integer.sum (map length (take kk perm_ctrss))) kks;
 
     val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
-    val perm_Cs = map (body_type o #ctor_recT) perm_basic_lfp_sugars;
-    val perm_fun_arg_Tssss =
-      binder_fun_types (#ctor_recT (hd perm_basic_lfp_sugars))
-      |> map3 mk_iter_fun_arg_types perm_ns perm_mss
-      |> map2 (map2 (map2 unzip_recT)) perm_ctr_Tsss;
+    val perm_Cs = map #C perm_basic_lfp_sugars;
+    val perm_fun_arg_Tssss = map #fun_arg_Tsss perm_basic_lfp_sugars;
 
     fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
     fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;
diff -r 6a1cbddebf86 -r 4a940ebceef8 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Wed Feb 19 08:33:59 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Wed Feb 19 08:34:32 2014 +0100
@@ -19,10 +19,9 @@
 fun is_new_datatype ctxt s =
   (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
 
-fun basic_lfp_sugar_of ({T, fp_res = {xtor_co_iterss = ctor_iterss, ...}, fp_res_index, ctr_defs,
-    ctr_sugar, co_iters = iters, co_iter_thmss = iter_thmss, ...} : fp_sugar) =
-  {T = T, fp_res_index = fp_res_index,
-   ctor_recT = fastype_of (co_rec_of (nth ctor_iterss fp_res_index)), ctr_defs = ctr_defs,
+fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_defs, ctr_sugar, co_iters = iters,
+    co_iter_thmss = iter_thmss, ...} : fp_sugar) =
+  {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_defs = ctr_defs,
    ctr_sugar = ctr_sugar, recx = co_rec_of iters, rec_thms = co_rec_of iter_thmss};
 
 fun get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0 =
@@ -31,11 +30,26 @@
           fp_sugars as {nested_bnfs, co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)),
          lthy) =
       nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy0;
+
+    val Ts = map #T fp_sugars;
+    val Cs = map (body_type o fastype_of o co_rec_of o #co_iters) fp_sugars;
+    val Ts_Cs = Ts ~~ Cs;
+
+    fun zip_recT (T as Type (s, Ts)) =
+        (case AList.lookup (op =) Ts_Cs T of
+          SOME C => [T, C]
+        | NONE => [Type (s, map (HOLogic.mk_tupleT o zip_recT) Ts)])
+      | zip_recT T = [T];
+
+    val ctrss = map (#ctrs o #ctr_sugar) fp_sugars;
+    val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
+    val fun_arg_Tssss = map (map (map zip_recT)) ctr_Tsss;
+
     val nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs;
     val nested_map_comps = map map_comp_of_bnf nested_bnfs;
   in
-    (missing_arg_Ts, perm0_kks, map basic_lfp_sugar_of fp_sugars, nested_map_idents,
-     nested_map_comps, induct_thm, is_some lfp_sugar_thms, lthy)
+    (missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
+     nested_map_idents, nested_map_comps, induct_thm, is_some lfp_sugar_thms, lthy)
   end;
 
 exception NOT_A_MAP of term;