1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 11 17:40:55 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 11 17:59:41 2013 +0100
     1.3 @@ -116,6 +116,8 @@
     1.4  
     1.5      fun incompatible_calls t1 t2 =
     1.6        error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ qsotm t1 ^ " vs. " ^ qsotm t2);
     1.7 +    fun nested_self_call t =
     1.8 +      error ("Unsupported nested self-call " ^ qsotm t);
     1.9  
    1.10      val b_names = map Binding.name_of bs;
    1.11      val fp_b_names = map base_name_of_typ fpTs;
    1.12 @@ -155,23 +157,27 @@
    1.13          | kk => nth Xs kk)
    1.14        | freeze_fpTs_simple T = T;
    1.15  
    1.16 -    fun freeze_fpTs_map (callss, (live_call :: _, dead_calls)) s Ts =
    1.17 -      (List.app (check_call_dead live_call) dead_calls;
    1.18 -       Type (s, map2 freeze_fpTs (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
    1.19 -         (transpose callss)) Ts))
    1.20 -    and freeze_fpTs calls (T as Type (s, Ts)) =
    1.21 +    fun freeze_fpTs_map (fpT as Type (_, Ts')) (callss, (live_call :: _, dead_calls))
    1.22 +        (T as Type (s, Ts)) =
    1.23 +      if Ts' = Ts then
    1.24 +        nested_self_call live_call
    1.25 +      else
    1.26 +        (List.app (check_call_dead live_call) dead_calls;
    1.27 +         Type (s, map2 (freeze_fpTs fpT) (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
    1.28 +           (transpose callss)) Ts))
    1.29 +    and freeze_fpTs fpT calls (T as Type (s, _)) =
    1.30          (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
    1.31            ([], _) =>
    1.32            (case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of
    1.33              ([], _) => freeze_fpTs_simple T
    1.34 -          | callsp => freeze_fpTs_map callsp s Ts)
    1.35 -        | callsp => freeze_fpTs_map callsp s Ts)
    1.36 -      | freeze_fpTs _ T = T;
    1.37 +          | callsp => freeze_fpTs_map fpT callsp T)
    1.38 +        | callsp => freeze_fpTs_map fpT callsp T)
    1.39 +      | freeze_fpTs _ _ T = T;
    1.40  
    1.41      val ctr_Tsss = map (map binder_types) ctr_Tss;
    1.42 -    val ctrXs_Tsss = map2 (map2 (map2 freeze_fpTs)) callssss ctr_Tsss;
    1.43 +    val ctrXs_Tsss = map3 (map2 o map2 o freeze_fpTs) fpTs callssss ctr_Tsss;
    1.44      val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
    1.45 -    val Ts = map (body_type o hd) ctr_Tss;
    1.46 +    val ctr_Ts = map (body_type o hd) ctr_Tss;
    1.47  
    1.48      val ns = map length ctr_Tsss;
    1.49      val kss = map (fn n => 1 upto n) ns;
    1.50 @@ -208,7 +214,7 @@
    1.51                (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
    1.52            |>> split_list;
    1.53  
    1.54 -        val rho = tvar_subst thy Ts fpTs;
    1.55 +        val rho = tvar_subst thy ctr_Ts fpTs;
    1.56          val ctr_sugar_phi = Morphism.compose (Morphism.typ_morphism (Term.typ_subst_TVars rho))
    1.57              (Morphism.term_morphism (Term.subst_TVars rho));
    1.58          val inst_ctr_sugar = morph_ctr_sugar ctr_sugar_phi;