--- a/src/HOL/Tools/BNF/bnf_def.ML Mon Jun 26 23:12:43 2017 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Tue Jun 27 00:07:34 2017 +0200
@@ -1230,10 +1230,14 @@
val (bnf_b, key) =
if Binding.is_empty bnf_b then
(case T_rhs of
- Type (C, Ts) => if forall (can dest_TFree) Ts
- then (Binding.qualified_name C, C) else err T_rhs
+ Type (C, Ts) =>
+ if forall (can dest_TFree) Ts andalso not (has_duplicates (op =) Ts) then
+ (Binding.qualified_name C, C)
+ else
+ err T_rhs
| T => err T)
- else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b);
+ else
+ (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b);
val (((alphas, betas, deads, Calpha),
(bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel, bnf_pred),