disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
authorwenzelm
Sat Mar 27 16:01:45 2010 +0100 (2010-03-27)
changeset 359877c728daf4876
parent 35986 b7fcca3d9a44
child 35988 76ca601c941e
disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Sat Mar 27 15:47:57 2010 +0100
     1.2 +++ b/src/Pure/theory.ML	Sat Mar 27 16:01:45 2010 +0100
     1.3 @@ -159,10 +159,17 @@
     1.4      val t = Sign.cert_prop thy raw_tm
     1.5        handle TYPE (msg, _, _) => error msg
     1.6          | TERM (msg, _) => error msg;
     1.7 +    val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
     1.8 +
     1.9 +    val bad_sorts =
    1.10 +      rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
    1.11 +    val _ = null bad_sorts orelse
    1.12 +      error ("Illegal sort constraints in primitive specification: " ^
    1.13 +        commas (map (setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy)) bad_sorts));
    1.14    in
    1.15 -    Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
    1.16      (b, Sign.no_vars (Syntax.pp_global thy) t)
    1.17 -  end;
    1.18 +  end handle ERROR msg =>
    1.19 +    cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
    1.20  
    1.21  fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
    1.22    let