clarified errors;
authorwenzelm
Fri Sep 21 17:48:39 2018 +0200 (13 months ago)
changeset 690275ea3f424e787
parent 69026 6e2f9f62aafd
child 69028 f440bedb8e45
child 69030 1eb517214deb
clarified errors;
src/Pure/Thy/export_theory.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Fri Sep 21 16:47:03 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Fri Sep 21 17:48:39 2018 +0200
     1.3 @@ -277,8 +277,17 @@
     1.4          val axioms = locale_axioms thy loc;
     1.5          val args = map #1 params;
     1.6          val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) (rev type_params));
     1.7 +        val _ =
     1.8 +          (case duplicates (eq_fst op =) typargs of
     1.9 +            [] => ()
    1.10 +          | dups =>
    1.11 +              let val print = Syntax.string_of_typ (Config.put show_sorts true thy_ctxt) o TFree
    1.12 +              in error ("Duplicate type parameters " ^ commas (map print dups)) end);
    1.13          val used = fold Name.declare (map #1 typargs @ map #1 args) Name.context;
    1.14 -      in encode_locale used (typargs, args, axioms) end;
    1.15 +      in encode_locale used (typargs, args, axioms) end
    1.16 +      handle ERROR msg =>
    1.17 +        cat_error msg ("The error(s) above occurred in locale " ^
    1.18 +          quote (Locale.markup_name thy_ctxt loc));
    1.19  
    1.20      val _ =
    1.21        export_entities "locales" (SOME oo export_locale) Locale.locale_space