1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
     1.3 @@ -139,27 +139,27 @@
     1.4        fun check_call_dead live_call call =
     1.5          if null (get_indices call) then () else incompatible_calls live_call call;
     1.6  
     1.7 -      fun freeze_fp_simple (T as Type (s, Ts)) =
     1.8 +      fun freeze_fpTs_simple (T as Type (s, Ts)) =
     1.9            (case find_index (curry (op =) T) fpTs of
    1.10 -            ~1 => Type (s, map freeze_fp_simple Ts)
    1.11 +            ~1 => Type (s, map freeze_fpTs_simple Ts)
    1.12            | kk => nth Xs kk)
    1.13 -        | freeze_fp_simple T = T;
    1.14 +        | freeze_fpTs_simple T = T;
    1.15  
    1.16 -      fun freeze_fp_map (callss, (live_call :: _, dead_calls)) s Ts =
    1.17 +      fun freeze_fpTs_map (callss, (live_call :: _, dead_calls)) s Ts =
    1.18          (List.app (check_call_dead live_call) dead_calls;
    1.19 -         Type (s, map2 freeze_fp (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
    1.20 +         Type (s, map2 freeze_fpTs (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
    1.21             (transpose callss)) Ts))
    1.22 -      and freeze_fp calls (T as Type (s, Ts)) =
    1.23 +      and freeze_fpTs calls (T as Type (s, Ts)) =
    1.24            (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
    1.25              ([], _) =>
    1.26              (case map_partition (try (snd o dest_abs_or_applied_map_or_ctr no_defs_lthy s)) calls of
    1.27 -              ([], _) => freeze_fp_simple T
    1.28 -            | callsp => freeze_fp_map callsp s Ts)
    1.29 -          | callsp => freeze_fp_map callsp s Ts)
    1.30 -        | freeze_fp _ T = T;
    1.31 +              ([], _) => freeze_fpTs_simple T
    1.32 +            | callsp => freeze_fpTs_map callsp s Ts)
    1.33 +          | callsp => freeze_fpTs_map callsp s Ts)
    1.34 +        | freeze_fpTs _ T = T;
    1.35  
    1.36        val ctr_Tsss = map (map binder_types) ctr_Tss;
    1.37 -      val ctrXs_Tsss = map2 (map2 (map2 freeze_fp)) callssss ctr_Tsss;
    1.38 +      val ctrXs_Tsss = map2 (map2 (map2 freeze_fpTs)) callssss ctr_Tsss;
    1.39        val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
    1.40        val Ts = map (body_type o hd) ctr_Tss;
    1.41  
    1.42 @@ -298,13 +298,18 @@
    1.43      val missing_Ts = perm_Ts |> subtract (op =) actual_Ts;
    1.44      val Ts = actual_Ts @ missing_Ts;
    1.45  
    1.46 -    fun generalize_type (T as Type (s, Ts)) (seen_lthy as (seen, lthy)) =
    1.47 -        (case AList.lookup (op =) seen T of
    1.48 -          SOME U => (U, seen_lthy)
    1.49 -        | NONE =>
    1.50 +    fun generalize_simple_type T (seen, lthy) =
    1.51 +      mk_TFrees 1 lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy)));
    1.52 +
    1.53 +    fun generalize_type T (seen_lthy as (seen, _)) =
    1.54 +      (case AList.lookup (op =) seen T of
    1.55 +        SOME U => (U, seen_lthy)
    1.56 +      | NONE =>
    1.57 +        (case T of
    1.58 +          Type (s, Ts) =>
    1.59            if exists_subtype_in Ts T then fold_map generalize_type Ts seen_lthy |>> curry Type s
    1.60 -          else mk_TFrees 1 lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy))))
    1.61 -      | generalize_type T seen_lthy = (T, seen_lthy);
    1.62 +          else generalize_simple_type T seen_lthy
    1.63 +        | _ => generalize_simple_type T seen_lthy));
    1.64  
    1.65      val (perm_Us, _) = fold_map generalize_type perm_Ts ([], lthy);
    1.66