merged

--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 11 17:44:21 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 11 18:37:56 2013 +0100
@@ -116,6 +116,8 @@
 
     fun incompatible_calls t1 t2 =
       error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ qsotm t1 ^ " vs. " ^ qsotm t2);
+    fun nested_self_call t =
+      error ("Unsupported nested self-call " ^ qsotm t);
 
     val b_names = map Binding.name_of bs;
     val fp_b_names = map base_name_of_typ fpTs;
@@ -132,9 +134,9 @@
 
     val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
     val mapss = map (of_fp_sugar #mapss) fp_sugars0;
-    val ctr_sugars0 = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
+    val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
 
-    val ctrss = map #ctrs ctr_sugars0;
+    val ctrss = map #ctrs ctr_sugars;
     val ctr_Tss = map (map fastype_of) ctrss;
 
     val As' = fold (fold Term.add_tfreesT) ctr_Tss [];
@@ -155,23 +157,27 @@
         | kk => nth Xs kk)
       | freeze_fpTs_simple T = T;
 
-    fun freeze_fpTs_map (callss, (live_call :: _, dead_calls)) s Ts =
-      (List.app (check_call_dead live_call) dead_calls;
-       Type (s, map2 freeze_fpTs (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
-         (transpose callss)) Ts))
-    and freeze_fpTs calls (T as Type (s, Ts)) =
+    fun freeze_fpTs_map (fpT as Type (_, Ts')) (callss, (live_call :: _, dead_calls))
+        (T as Type (s, Ts)) =
+      if Ts' = Ts then
+        nested_self_call live_call
+      else
+        (List.app (check_call_dead live_call) dead_calls;
+         Type (s, map2 (freeze_fpTs fpT) (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
+           (transpose callss)) Ts))
+    and freeze_fpTs fpT calls (T as Type (s, _)) =
         (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
           ([], _) =>
           (case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of
             ([], _) => freeze_fpTs_simple T
-          | callsp => freeze_fpTs_map callsp s Ts)
-        | callsp => freeze_fpTs_map callsp s Ts)
-      | freeze_fpTs _ T = T;
+          | callsp => freeze_fpTs_map fpT callsp T)
+        | callsp => freeze_fpTs_map fpT callsp T)
+      | freeze_fpTs _ _ T = T;
 
     val ctr_Tsss = map (map binder_types) ctr_Tss;
-    val ctrXs_Tsss = map2 (map2 (map2 freeze_fpTs)) callssss ctr_Tsss;
+    val ctrXs_Tsss = map3 (map2 o map2 o freeze_fpTs) fpTs callssss ctr_Tsss;
     val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
-    val Ts = map (body_type o hd) ctr_Tss;
+    val ctr_Ts = map (body_type o hd) ctr_Tss;
 
     val ns = map length ctr_Tsss;
     val kss = map (fn n => 1 upto n) ns;
@@ -208,13 +214,6 @@
               (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
           |>> split_list;
 
-        val rho = tvar_subst thy Ts fpTs;
-        val ctr_sugar_phi = Morphism.compose (Morphism.typ_morphism (Term.typ_subst_TVars rho))
-            (Morphism.term_morphism (Term.subst_TVars rho));
-        val inst_ctr_sugar = morph_ctr_sugar ctr_sugar_phi;
-
-        val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
-
         val ((co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
               sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
           if fp = Least_FP then

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Nov 11 17:44:21 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Nov 11 18:37:56 2013 +0100
@@ -10,7 +10,7 @@
 sig
   val indexed: 'a list -> int -> int list * int
   val indexedd: 'a list list -> int -> int list list * int
-  val indexeddd: ''a list list list -> int -> int list list list * int
+  val indexeddd: 'a list list list -> int -> int list list list * int
   val indexedddd: 'a list list list list -> int -> int list list list list * int
   val find_index_eq: ''a list -> ''a -> int
   val finds: ('a * 'b -> bool) -> 'a list -> 'b list -> ('a * 'b list) list * 'b list