gracefully handle one more error condition
authorblanchet
Sun, 11 Aug 2013 23:35:59 +0200
changeset 52960 f583d7b72d4e
parent 52959 8d581fd1b46f
child 52961 bb8787b20437
gracefully handle one more error condition
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sun Aug 11 23:35:59 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sun Aug 11 23:35:59 2013 +0200
@@ -1000,6 +1000,9 @@
     val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
     val set_bss = map (map fst o type_args_named_constrained_of) specs;
 
+    val _ = has_duplicates (op =) unsorted_As andalso
+      error ("Duplicate parameters in " ^ co_prefix fp ^ "datatype specification");
+
     val bad_args =
       map (Logic.type_map (singleton (Variable.polymorphic no_defs_lthy0))) unsorted_As
       |> filter_out Term.is_TVar;