--- a/src/HOL/Tools/Function/function_common.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Sun Sep 05 21:41:24 2010 +0200
@@ -288,7 +288,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_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
+ Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
val _ = map check_sorts fixes
in