# HG changeset patch
# User blanchet
# Date 1498514854 -7200
# Node ID 4a5589dd8e1a8747fc63a0a499d2df6beb1bb996
# Parent  c8604c9f3a8ae66d2ee98d4a33df475d368ee34c
more error checking

diff -r c8604c9f3a8a -r 4a5589dd8e1a src/HOL/BNF_Def.thy
--- 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)"
diff -r c8604c9f3a8a -r 4a5589dd8e1a src/HOL/Tools/BNF/bnf_def.ML
--- 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),