src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Thu Feb 27 11:41:32 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Thu Feb 27 13:04:57 2014 +0100
@@ -26,26 +26,26 @@
   {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 =
+fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 =
   let
     val ((missing_arg_Ts, perm0_kks,
           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;
+      nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0;
 
     val Ts = map #T fp_sugars;
+    val Xs = map #X fp_sugars;
     val Cs = map (body_type o fastype_of o co_rec_of o #co_iters) fp_sugars;
-    val Ts_Cs = Ts ~~ Cs;
+    val Xs_TCs = Xs ~~ (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];
+    fun zip_recT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_recT) Us)]
+      | zip_recT U =
+        (case AList.lookup (op =) Xs_TCs U of
+          SOME (T, C) => [T, C]
+        | NONE => [U]);
 
-    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 ctrXs_Tsss = map #ctrXs_Tss fp_sugars;
+    val fun_arg_Tssss = map (map (map zip_recT)) ctrXs_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;