diff -r ecb746bca732 -r 5b21661fe618 src/HOL/Tools/Function/fundef_common.ML
--- a/src/HOL/Tools/Function/fundef_common.ML	Sat Oct 17 15:55:57 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_common.ML	Sat Oct 17 15:57:51 2009 +0200
@@ -267,7 +267,7 @@
           Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
           orelse error (cat_lines 
           ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
-           setmp show_sorts true (Syntax.string_of_typ ctxt) fT])
+           setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
 
       val _ = map check_sorts fixes
     in