src/Pure/Thy/export_theory.ML
changeset 69028 f440bedb8e45
parent 69027 5ea3f424e787
child 69029 aec64b88e708
     1.1 --- a/src/Pure/Thy/export_theory.ML	Fri Sep 21 17:48:39 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Fri Sep 21 21:06:23 2018 +0200
     1.3 @@ -276,13 +276,16 @@
     1.4        let
     1.5          val axioms = locale_axioms thy loc;
     1.6          val args = map #1 params;
     1.7 +
     1.8          val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) (rev type_params));
     1.9 +        val typargs_dups =
    1.10 +          AList.group (op =) typargs |> filter (fn (_, [_]) => false | _ => true)
    1.11 +            |> maps (fn (x, ys) => map (pair x) ys);
    1.12 +        val typargs_print = Syntax.string_of_typ (Config.put show_sorts true thy_ctxt) o TFree;
    1.13          val _ =
    1.14 -          (case duplicates (eq_fst op =) typargs of
    1.15 -            [] => ()
    1.16 -          | dups =>
    1.17 -              let val print = Syntax.string_of_typ (Config.put show_sorts true thy_ctxt) o TFree
    1.18 -              in error ("Duplicate type parameters " ^ commas (map print dups)) end);
    1.19 +          if null typargs_dups then ()
    1.20 +          else error ("Duplicate type parameters " ^ commas (map typargs_print typargs_dups));
    1.21 +
    1.22          val used = fold Name.declare (map #1 typargs @ map #1 args) Name.context;
    1.23        in encode_locale used (typargs, args, axioms) end
    1.24        handle ERROR msg =>