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 @@ -295,10 +295,19 @@
     1.4        | check_enrich_with_mutuals _ (T :: _) = not_co_datatype T;
     1.5  
     1.6      val perm_Ts = check_enrich_with_mutuals [] perm_actual_Ts;
     1.7 -
     1.8      val missing_Ts = perm_Ts |> subtract (op =) actual_Ts;
     1.9      val Ts = actual_Ts @ missing_Ts;
    1.10  
    1.11 +    fun generalize_type (T as Type (s, Ts)) (seen_lthy as (seen, lthy)) =
    1.12 +        (case AList.lookup (op =) seen T of
    1.13 +          SOME U => (U, seen_lthy)
    1.14 +        | NONE =>
    1.15 +          if exists_subtype_in Ts T then fold_map generalize_type Ts seen_lthy |>> curry Type s
    1.16 +          else mk_TFrees 1 lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy))))
    1.17 +      | generalize_type T seen_lthy = (T, seen_lthy);
    1.18 +
    1.19 +    val (perm_Us, _) = fold_map generalize_type perm_Ts ([], lthy);
    1.20 +
    1.21      val nn = length Ts;
    1.22      val kks = 0 upto nn - 1;
    1.23  
    1.24 @@ -318,7 +327,7 @@
    1.25      val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
    1.26  
    1.27      val ((perm_fp_sugars, fp_sugar_thms), lthy) =
    1.28 -      mutualize_fp_sugars has_nested fp perm_bs perm_Ts get_perm_indices perm_callssss
    1.29 +      mutualize_fp_sugars has_nested fp perm_bs perm_Us get_perm_indices perm_callssss
    1.30          perm_fp_sugars0 lthy;
    1.31  
    1.32      val fp_sugars = unpermute perm_fp_sugars;