src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Aug 06 15:50:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Aug 06 15:50:23 2013 +0200
@@ -361,32 +361,42 @@
     ([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy)
   end;
 
-fun mk_coiters_args_types Cs ns mss dtor_coiter_fun_Tss lthy =
+fun unzip_corecT Cs (T as Type (@{type_name sum}, Ts as [_, U])) =
+    if member (op =) Cs U then Ts else [T]
+  | unzip_corecT _ T = [T];
+
+fun mk_coiter_fun_arg_typessss_typesss_typessss Cs ns mss maybe_unzipT fun_Ts =
   let
     (*avoid "'a itself" arguments in coiterators and corecursors*)
     fun repair_arity [0] = [1]
       | repair_arity ms = ms;
 
-    fun unzip_corecT (T as Type (@{type_name sum}, Ts as [_, U])) =
-        if member (op =) Cs U then Ts else [T]
-      | unzip_corecT T = [T];
+    val f_sum_prod_Ts = map range_type fun_Ts;
+    val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts;
+    val f_Tsss = map2 (map2 dest_tupleT o repair_arity) mss f_prod_Tss;
+    val f_Tssss = map2 (fn C => map (map (map (curry (op -->) C) o maybe_unzipT))) Cs f_Tsss;
+    val q_Tssss =
+      map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss;
+  in
+    (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts)
+  end;
 
+fun mk_coiters_args_types Cs ns mss dtor_coiter_fun_Tss lthy =
+  let
     val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
 
     fun mk_types maybe_unzipT get_Ts =
       let
         val fun_Ts = map get_Ts dtor_coiter_fun_Tss;
-        val f_sum_prod_Ts = map range_type fun_Ts;
-        val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts;
-        val f_Tsss = map2 (map2 dest_tupleT o repair_arity) mss f_prod_Tss;
-        val f_Tssss = map2 (fn C => map (map (map (curry (op -->) C) o maybe_unzipT))) Cs f_Tsss;
-        val q_Tssss =
-          map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss;
+        val (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) =
+          mk_coiter_fun_arg_typessss_typesss_typessss Cs ns mss maybe_unzipT fun_Ts;
         val pf_Tss = map3 flat_corec_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
-      in (q_Tssss, f_Tsss, f_Tssss, (f_sum_prod_Ts, pf_Tss)) end;
+      in
+        (q_Tssss, f_Tsss, f_Tssss, (f_sum_prod_Ts, pf_Tss))
+      end;
 
     val (r_Tssss, g_Tsss, g_Tssss, unfold_types) = mk_types single un_fold_of;
-    val (s_Tssss, h_Tsss, h_Tssss, corec_types) = mk_types unzip_corecT co_rec_of;
+    val (s_Tssss, h_Tsss, h_Tssss, corec_types) = mk_types (unzip_corecT Cs) co_rec_of;
 
     val ((((Free (z, _), cs), pss), gssss), lthy) =
       lthy