diff -r ecb746bca732 -r 5b21661fe618 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/axclass.ML	Sat Oct 17 15:57:51 2009 +0200
@@ -438,7 +438,7 @@
     fun check_constraint (a, S) =
       if Sign.subsort thy (super, S) then ()
       else error ("Sort constraint of type variable " ^
-        setmp show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^
+        setmp_CRITICAL show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^
         " needs to be weaker than " ^ Pretty.string_of_sort pp super);