# HG changeset patch
# User wenzelm
# Date 1269702105 -3600
# Node ID 7c728daf4876a0a72e4714ad36a586e472cf6571
# Parent  b7fcca3d9a441af04c807d547fbc59f42811e5ab
disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;

diff -r b7fcca3d9a44 -r 7c728daf4876 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Mar 27 15:47:57 2010 +0100
+++ b/src/Pure/theory.ML	Sat Mar 27 16:01:45 2010 +0100
@@ -159,10 +159,17 @@
     val t = Sign.cert_prop thy raw_tm
       handle TYPE (msg, _, _) => error msg
         | TERM (msg, _) => error msg;
+    val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
+
+    val bad_sorts =
+      rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
+    val _ = null bad_sorts orelse
+      error ("Illegal sort constraints in primitive specification: " ^
+        commas (map (setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy)) bad_sorts));
   in
-    Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
     (b, Sign.no_vars (Syntax.pp_global thy) t)
-  end;
+  end handle ERROR msg =>
+    cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
 
 fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
   let