# HG changeset patch
# User wenzelm
# Date 1537556783 -7200
# Node ID f440bedb8e4595efbb5b5ccab8dde469d972e4bc
# Parent  5ea3f424e787bdf9565f1dfe075dafad6be3b6f3
clarified error;

diff -r 5ea3f424e787 -r f440bedb8e45 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Fri Sep 21 17:48:39 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri Sep 21 21:06:23 2018 +0200
@@ -276,13 +276,16 @@
       let
         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 typargs_dups =
+          AList.group (op =) typargs |> filter (fn (_, [_]) => false | _ => true)
+            |> maps (fn (x, ys) => map (pair x) ys);
+        val typargs_print = Syntax.string_of_typ (Config.put show_sorts true thy_ctxt) o TFree;
         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);
+          if null typargs_dups then ()
+          else error ("Duplicate type parameters " ^ commas (map typargs_print typargs_dups));
+
         val used = fold Name.declare (map #1 typargs @ map #1 args) Name.context;
       in encode_locale used (typargs, args, axioms) end
       handle ERROR msg =>