# HG changeset patch
# User blanchet
# Date 1376256959 -7200
# Node ID f583d7b72d4e9ae5a8e9883595d0d34924977b1c
# Parent  8d581fd1b46f0b4efe606f11484cdc3fb4b788a9
gracefully handle one more error condition

diff -r 8d581fd1b46f -r f583d7b72d4e 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;