1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Nov 05 15:30:53 2013 +1100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
     1.3 @@ -1000,7 +1000,7 @@
     1.4  
     1.5      val qsoty = quote o Syntax.string_of_typ fake_lthy;
     1.6  
     1.7 -    val _ = (case duplicates (op =) unsorted_As of [] => ()
     1.8 +    val _ = (case Library.duplicates (op =) unsorted_As of [] => ()
     1.9        | A :: _ => error ("Duplicate type parameter " ^ qsoty A ^ " in " ^ co_prefix fp ^
    1.10            "datatype specification"));
    1.11  
    1.12 @@ -1013,7 +1013,7 @@
    1.13  
    1.14      val mixfixes = map mixfix_of specs;
    1.15  
    1.16 -    val _ = (case duplicates Binding.eq_name fp_bs of [] => ()
    1.17 +    val _ = (case Library.duplicates Binding.eq_name fp_bs of [] => ()
    1.18        | b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b)));
    1.19  
    1.20      val ctr_specss = map ctr_specs_of specs;

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 15:30:53 2013 +1100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
     2.3 @@ -97,7 +97,7 @@
     2.4  (* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
     2.5     as deads? *)
     2.6  fun mutualize_fp_sugars has_nested fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 =
     2.7 -  if has_nested orelse has_duplicates (op =) fpTs then
     2.8 +  if has_nested then
     2.9      let
    2.10        val thy = Proof_Context.theory_of no_defs_lthy0;
    2.11  
    2.12 @@ -136,15 +136,15 @@
    2.13          |> mk_TFrees nn
    2.14          ||>> variant_tfrees fp_b_names;
    2.15  
    2.16 -      fun freeze_fp_default (T as Type (s, Ts)) =
    2.17 -          (case find_index (curry (op =) T) fpTs of
    2.18 -            ~1 => Type (s, map freeze_fp_default Ts)
    2.19 -          | kk => nth Xs kk)
    2.20 -        | freeze_fp_default T = T;
    2.21 -
    2.22        fun check_call_dead live_call call =
    2.23          if null (get_indices call) then () else incompatible_calls live_call call;
    2.24  
    2.25 +      fun freeze_fp_simple (T as Type (s, Ts)) =
    2.26 +          (case find_index (curry (op =) T) fpTs of
    2.27 +            ~1 => Type (s, map freeze_fp_simple Ts)
    2.28 +          | kk => nth Xs kk)
    2.29 +        | freeze_fp_simple T = T;
    2.30 +
    2.31        fun freeze_fp_map (callss, (live_call :: _, dead_calls)) s Ts =
    2.32          (List.app (check_call_dead live_call) dead_calls;
    2.33           Type (s, map2 freeze_fp (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
    2.34 @@ -153,7 +153,7 @@
    2.35            (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
    2.36              ([], _) =>
    2.37              (case map_partition (try (snd o dest_abs_or_applied_map_or_ctr no_defs_lthy s)) calls of
    2.38 -              ([], _) => freeze_fp_default T
    2.39 +              ([], _) => freeze_fp_simple T
    2.40              | callsp => freeze_fp_map callsp s Ts)
    2.41            | callsp => freeze_fp_map callsp s Ts)
    2.42          | freeze_fp _ T = T;
    2.43 @@ -257,6 +257,7 @@
    2.44      val qsoty = quote o Syntax.string_of_typ lthy;
    2.45      val qsotys = space_implode " or " o map qsoty;
    2.46  
    2.47 +    fun duplicate_datatype T = error (qsoty T ^ " is not mutually recursive with itself");
    2.48      fun not_co_datatype0 T = error (qsoty T ^ " is not a " ^ co_prefix fp ^ "datatype");
    2.49      fun not_co_datatype (T as Type (s, _)) =
    2.50          if fp = Least_FP andalso
    2.51 @@ -269,6 +270,8 @@
    2.52        error (qsotys Ts1 ^ " is neither mutually recursive with nor nested recursive via " ^
    2.53          qsotys Ts2);
    2.54  
    2.55 +    val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T);
    2.56 +
    2.57      val perm_actual_Ts as Type (_, ty_args0) :: _ =
    2.58        sort (int_ord o pairself Term.size_of_typ) actual_Ts;
    2.59