1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 15:30:53 2013 +1100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
     1.3 @@ -97,7 +97,7 @@
     1.4  (* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
     1.5     as deads? *)
     1.6  fun mutualize_fp_sugars has_nested fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 =
     1.7 -  if has_nested orelse has_duplicates (op =) fpTs then
     1.8 +  if has_nested then
     1.9      let
    1.10        val thy = Proof_Context.theory_of no_defs_lthy0;
    1.11  
    1.12 @@ -136,15 +136,15 @@
    1.13          |> mk_TFrees nn
    1.14          ||>> variant_tfrees fp_b_names;
    1.15  
    1.16 -      fun freeze_fp_default (T as Type (s, Ts)) =
    1.17 -          (case find_index (curry (op =) T) fpTs of
    1.18 -            ~1 => Type (s, map freeze_fp_default Ts)
    1.19 -          | kk => nth Xs kk)
    1.20 -        | freeze_fp_default T = T;
    1.21 -
    1.22        fun check_call_dead live_call call =
    1.23          if null (get_indices call) then () else incompatible_calls live_call call;
    1.24  
    1.25 +      fun freeze_fp_simple (T as Type (s, Ts)) =
    1.26 +          (case find_index (curry (op =) T) fpTs of
    1.27 +            ~1 => Type (s, map freeze_fp_simple Ts)
    1.28 +          | kk => nth Xs kk)
    1.29 +        | freeze_fp_simple T = T;
    1.30 +
    1.31        fun freeze_fp_map (callss, (live_call :: _, dead_calls)) s Ts =
    1.32          (List.app (check_call_dead live_call) dead_calls;
    1.33           Type (s, map2 freeze_fp (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
    1.34 @@ -153,7 +153,7 @@
    1.35            (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
    1.36              ([], _) =>
    1.37              (case map_partition (try (snd o dest_abs_or_applied_map_or_ctr no_defs_lthy s)) calls of
    1.38 -              ([], _) => freeze_fp_default T
    1.39 +              ([], _) => freeze_fp_simple T
    1.40              | callsp => freeze_fp_map callsp s Ts)
    1.41            | callsp => freeze_fp_map callsp s Ts)
    1.42          | freeze_fp _ T = T;
    1.43 @@ -257,6 +257,7 @@
    1.44      val qsoty = quote o Syntax.string_of_typ lthy;
    1.45      val qsotys = space_implode " or " o map qsoty;
    1.46  
    1.47 +    fun duplicate_datatype T = error (qsoty T ^ " is not mutually recursive with itself");
    1.48      fun not_co_datatype0 T = error (qsoty T ^ " is not a " ^ co_prefix fp ^ "datatype");
    1.49      fun not_co_datatype (T as Type (s, _)) =
    1.50          if fp = Least_FP andalso
    1.51 @@ -269,6 +270,8 @@
    1.52        error (qsotys Ts1 ^ " is neither mutually recursive with nor nested recursive via " ^
    1.53          qsotys Ts2);
    1.54  
    1.55 +    val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T);
    1.56 +
    1.57      val perm_actual_Ts as Type (_, ty_args0) :: _ =
    1.58        sort (int_ord o pairself Term.size_of_typ) actual_Ts;
    1.59