# HG changeset patch
# User wenzelm
# Date 1537544919 -7200
# Node ID 5ea3f424e787bdf9565f1dfe075dafad6be3b6f3
# Parent  6e2f9f62aafdaa2a6dc5e23afc06539ab7d570b4
clarified errors;

diff -r 6e2f9f62aafd -r 5ea3f424e787 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Fri Sep 21 16:47:03 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri Sep 21 17:48:39 2018 +0200
@@ -277,8 +277,17 @@
         val axioms = locale_axioms thy loc;
         val args = map #1 params;
         val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) (rev type_params));
+        val _ =
+          (case duplicates (eq_fst op =) typargs of
+            [] => ()
+          | dups =>
+              let val print = Syntax.string_of_typ (Config.put show_sorts true thy_ctxt) o TFree
+              in error ("Duplicate type parameters " ^ commas (map print dups)) end);
         val used = fold Name.declare (map #1 typargs @ map #1 args) Name.context;
-      in encode_locale used (typargs, args, axioms) end;
+      in encode_locale used (typargs, args, axioms) end
+      handle ERROR msg =>
+        cat_error msg ("The error(s) above occurred in locale " ^
+          quote (Locale.markup_name thy_ctxt loc));
 
     val _ =
       export_entities "locales" (SOME oo export_locale) Locale.locale_space