src/Pure/theory.ML

--- a/src/Pure/theory.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/theory.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -161,11 +161,13 @@
         | TERM (msg, _) => error msg;
     val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
 
+    val ctxt = Syntax.init_pretty_global thy
+      |> Config.put show_sorts true;
     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));
+        commas (map (Syntax.string_of_typ ctxt) bad_sorts));
   in
     (b, Sign.no_vars (Syntax.init_pretty_global thy) t)
   end handle ERROR msg =>
@@ -217,18 +219,18 @@
       handle TYPE (msg, _, _) => error msg;
     val T' = Logic.varifyT_global T;
 
-    fun message txt =
+    val ctxt = Syntax.init_pretty_global thy;
+    fun message sorts txt =
       [Pretty.block [Pretty.str "Specification of constant ",
-        Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ_global thy T)],
+        Pretty.str c, Pretty.str " ::", Pretty.brk 1,
+        Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)],
         Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
   in
     if Sign.typ_instance thy (declT, T') then ()
     else if Type.raw_instance (declT, T') then
-      error (setmp_CRITICAL show_sorts true
-        message "imposes additional sort constraints on the constant declaration")
+      error (message true "imposes additional sort constraints on the constant declaration")
     else if overloaded then ()
-    else warning (message "is strictly less general than the declared type");
-    (c, T)
+    else warning (message false "is strictly less general than the declared type")
   end;
 
 
@@ -272,7 +274,7 @@
       | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
       | const_of _ = error "Attempt to finalize non-constant term";
     fun specify (c, T) = dependencies thy false NONE (c ^ " axiom") (c, T) [];
-    val finalize = specify o check_overloading thy overloaded o const_of o
+    val finalize = specify o tap (check_overloading thy overloaded) o const_of o
       Sign.cert_term thy o prep_term thy;
   in thy |> map_defs (fold finalize args) end;