# HG changeset patch
# User blanchet
# Date 1369787749 -7200
# Node ID b6a0668211f6911804bbcc850795c26e0f4478f7
# Parent  7facaee8586f33304d90f42e0789e57dd4ec72d1
more work on general recursors

diff -r 7facaee8586f -r b6a0668211f6 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed May 29 02:35:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed May 29 02:35:49 2013 +0200
@@ -266,7 +266,9 @@
 val project_recT = project_co_recT @{type_name prod};
 val project_corecT = project_co_recT @{type_name sum};
 
-fun unzip_recT fpTs = meta_unzip_rec I (project_recT fpTs fst) (project_recT fpTs snd) I fpTs;
+fun unzip_recT fpTs (T as Type (@{type_name prod}, Ts as [T', _])) =
+    if member (op =) fpTs T' then Ts else [T]
+  | unzip_recT _ T = [T];
 
 fun mk_fun_arg_typess n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
 
@@ -275,7 +277,7 @@
   #> map3 mk_fun_arg_typess ns mss
   #> map (map (map (unzip_recT fpTs)));
 
-fun mk_fold_rec_args_types Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy =
+fun mk_fold_rec_args_types fpTs Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy =
   let
     val Css = map2 replicate ns Cs;
     val y_Tsss = map3 mk_fun_arg_typess ns mss ctor_fold_fun_Ts;
@@ -287,13 +289,8 @@
       ||>> mk_Freesss "x" y_Tsss;
     val yssss = map (map (map single)) ysss;
 
-    (* ### *)
-    fun dest_rec_prodT (T as Type (@{type_name prod}, Us as [_, U])) =
-        if member (op =) Cs U then Us else [T]
-      | dest_rec_prodT T = [T];
-
     val z_Tssss =
-      map3 (fn n => fn ms => map2 (map dest_rec_prodT oo dest_tupleT) ms o
+      map3 (fn n => fn ms => map2 (map (unzip_recT fpTs) oo dest_tupleT) ms o
         dest_sumTN_balanced n o domain_type) ns mss ctor_rec_fun_Ts;
 
     val z_Tsss = map3 mk_fun_arg_typess ns mss ctor_rec_fun_Ts;
@@ -376,7 +373,7 @@
 
     val ((fold_rec_args_types, unfold_corec_args_types), lthy') =
       if fp = Least_FP then
-        mk_fold_rec_args_types Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
+        mk_fold_rec_args_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
         |>> (rpair NONE o SOME)
       else
         mk_unfold_corec_args_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
@@ -581,7 +578,7 @@
     val ctor_rec_fun_Ts = mk_fp_iter_fun_types (hd ctor_recs);
 
     val (((gss, _, _), (hss, _, _)), names_lthy0) =
-      mk_fold_rec_args_types Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy;
+      mk_fold_rec_args_types fpTs Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy;
 
     val ((((ps, ps'), xsss), us'), names_lthy) =
       names_lthy0