1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 16:53:40 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Nov 06 01:06:01 2013 +0100
     1.3 @@ -304,16 +304,16 @@
     1.4  
     1.5      val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T);
     1.6  
     1.7 -    val perm_actual_Ts as Type (_, ty_args0) :: _ =
     1.8 +    val perm_actual_Ts as Type (_, tyargs0) :: _ =
     1.9        sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts;
    1.10  
    1.11      fun check_enrich_with_mutuals _ [] = []
    1.12 -      | check_enrich_with_mutuals seen ((T as Type (T_name, ty_args)) :: Ts) =
    1.13 +      | check_enrich_with_mutuals seen ((T as Type (T_name, tyargs)) :: Ts) =
    1.14          (case fp_sugar_of lthy T_name of
    1.15            SOME ({fp = fp', fp_res = {Ts = Ts', ...}, ...}) =>
    1.16            if fp = fp' then
    1.17              let
    1.18 -              val mutual_Ts = map (fn Type (s, _) => Type (s, ty_args)) Ts';
    1.19 +              val mutual_Ts = map (fn Type (s, _) => Type (s, tyargs)) Ts';
    1.20                val _ =
    1.21                  seen = [] orelse exists (exists_subtype_in seen) mutual_Ts orelse
    1.22                  not_mutually_nested_rec mutual_Ts seen;
    1.23 @@ -330,21 +330,18 @@
    1.24      val missing_Ts = perm_Ts |> subtract (op =) actual_Ts;
    1.25      val Ts = actual_Ts @ missing_Ts;
    1.26  
    1.27 -    (* The name "'z" is likely not to clash with the context, resulting in more cache hits. *)
    1.28 -    fun generalize_simple_type T (seen, lthy) =
    1.29 -      variant_tfrees ["z"] lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy)));
    1.30 +    fun generalize_subtype T (tyarps_lthy as (tyarps, lthy)) =
    1.31 +      (* The name "'z" is unlikely to clash with the context, resulting in more cache hits. *)
    1.32 +      if exists_subtype_in Ts T then generalize_Type T tyarps_lthy
    1.33 +      else variant_tfrees ["z"] lthy |> (fn ([U], lthy) => (U, (tyarps, lthy)))
    1.34 +    and generalize_Type (Type (s, tyargs)) (tyarps_lthy as (tyarps, _)) =
    1.35 +      (case AList.lookup (op =) tyarps tyargs of
    1.36 +        SOME tyargs' => (Type (s, tyargs'), tyarps_lthy)
    1.37 +      | NONE => fold_map generalize_subtype tyargs tyarps_lthy
    1.38 +        |> (fn (tyargs', (tyarps, lthy)) =>
    1.39 +          (Type (s, tyargs'), ((tyargs, tyargs') :: tyarps, lthy))));
    1.40  
    1.41 -    fun generalize_type T (seen_lthy as (seen, _)) =
    1.42 -      (case AList.lookup (op =) seen T of
    1.43 -        SOME U => (U, seen_lthy)
    1.44 -      | NONE =>
    1.45 -        (case T of
    1.46 -          Type (s, Ts') =>
    1.47 -          if exists_subtype_in Ts T then fold_map generalize_type Ts' seen_lthy |>> curry Type s
    1.48 -          else generalize_simple_type T seen_lthy
    1.49 -        | _ => generalize_simple_type T seen_lthy));
    1.50 -
    1.51 -    val (perm_Us, _) = fold_map generalize_type perm_Ts ([], lthy);
    1.52 +    val (perm_Us, _) = fold_map generalize_Type perm_Ts ([], lthy);
    1.53  
    1.54      val nn = length Ts;
    1.55      val kks = 0 upto nn - 1;
    1.56 @@ -362,7 +359,7 @@
    1.57      val perm_callssss0 = permute callssss0;
    1.58      val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
    1.59  
    1.60 -    val has_nested = exists (fn Type (_, ty_args) => ty_args <> ty_args0) Ts;
    1.61 +    val has_nested = exists (fn Type (_, tyargs) => tyargs <> tyargs0) Ts;
    1.62      val perm_callssss = map2 indexify_callsss perm_fp_sugars0 perm_callssss0;
    1.63  
    1.64      val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;