--- a/src/HOL/BNF_Def.thy Mon Jun 26 23:12:43 2017 +0200
+++ b/src/HOL/BNF_Def.thy Tue Jun 27 00:07:34 2017 +0200
@@ -82,7 +82,7 @@
"vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
- by (rule ext) (auto simp only: comp_apply collect_def)
+ by (rule ext) (simp add: collect_def)
definition convol ("\<langle>(_,/ _)\<rangle>") where
"\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)"
--- 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),