1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Nov 06 01:57:22 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Nov 06 10:35:30 2013 +0100
     1.3 @@ -330,22 +330,6 @@
     1.4      val missing_Ts = perm_Ts |> subtract (op =) actual_Ts;
     1.5      val Ts = actual_Ts @ missing_Ts;
     1.6  
     1.7 -    (* The name "'z" is likely not to clash with the context, resulting in more cache hits. *)
     1.8 -    fun generalize_simple_type T (seen, lthy) =
     1.9 -      variant_tfrees ["z"] lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy)));
    1.10 -
    1.11 -    fun generalize_type T (seen_lthy as (seen, _)) =
    1.12 -      (case AList.lookup (op =) seen T of
    1.13 -        SOME U => (U, seen_lthy)
    1.14 -      | NONE =>
    1.15 -        (case T of
    1.16 -          Type (s, tyargs) =>
    1.17 -          if exists_subtype_in Ts T then fold_map generalize_type tyargs seen_lthy |>> curry Type s
    1.18 -          else generalize_simple_type T seen_lthy
    1.19 -        | _ => generalize_simple_type T seen_lthy));
    1.20 -
    1.21 -    val (perm_Us, _) = fold_map generalize_type perm_Ts ([], lthy);
    1.22 -
    1.23      val nn = length Ts;
    1.24      val kks = 0 upto nn - 1;
    1.25  
    1.26 @@ -368,7 +352,7 @@
    1.27      val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
    1.28  
    1.29      val ((perm_fp_sugars, fp_sugar_thms), lthy) =
    1.30 -      mutualize_fp_sugars has_nested fp perm_bs perm_Us get_perm_indices perm_callssss
    1.31 +      mutualize_fp_sugars has_nested fp perm_bs perm_Ts get_perm_indices perm_callssss
    1.32          perm_fp_sugars0 lthy;
    1.33  
    1.34      val fp_sugars = unpermute perm_fp_sugars;