1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Wed Nov 06 01:06:01 2013 +0100
1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Wed Nov 06 01:57:22 2013 +0100
1.3 @@ -330,18 +330,21 @@
1.4 val missing_Ts = perm_Ts |> subtract (op =) actual_Ts;
1.5 val Ts = actual_Ts @ missing_Ts;
1.6
1.7 - fun generalize_subtype T (tyarps_lthy as (tyarps, lthy)) =
1.8 - (* The name "'z" is unlikely to clash with the context, resulting in more cache hits. *)
1.9 - if exists_subtype_in Ts T then generalize_Type T tyarps_lthy
1.10 - else variant_tfrees ["z"] lthy |> (fn ([U], lthy) => (U, (tyarps, lthy)))
1.11 - and generalize_Type (Type (s, tyargs)) (tyarps_lthy as (tyarps, _)) =
1.12 - (case AList.lookup (op =) tyarps tyargs of
1.13 - SOME tyargs' => (Type (s, tyargs'), tyarps_lthy)
1.14 - | NONE => fold_map generalize_subtype tyargs tyarps_lthy
1.15 - |> (fn (tyargs', (tyarps, lthy)) =>
1.16 - (Type (s, tyargs'), ((tyargs, tyargs') :: tyarps, lthy))));
1.17 + (* The name "'z" is likely not to clash with the context, resulting in more cache hits. *)
1.18 + fun generalize_simple_type T (seen, lthy) =
1.19 + variant_tfrees ["z"] lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy)));
1.20
1.21 - val (perm_Us, _) = fold_map generalize_Type perm_Ts ([], lthy);
1.22 + fun generalize_type T (seen_lthy as (seen, _)) =
1.23 + (case AList.lookup (op =) seen T of
1.24 + SOME U => (U, seen_lthy)
1.25 + | NONE =>
1.26 + (case T of
1.27 + Type (s, tyargs) =>
1.28 + if exists_subtype_in Ts T then fold_map generalize_type tyargs seen_lthy |>> curry Type s
1.29 + else generalize_simple_type T seen_lthy
1.30 + | _ => generalize_simple_type T seen_lthy));
1.31 +
1.32 + val (perm_Us, _) = fold_map generalize_type perm_Ts ([], lthy);
1.33
1.34 val nn = length Ts;
1.35 val kks = 0 upto nn - 1;