diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Isar/class.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -164,7 +164,7 @@
         val Ss = Sorts.mg_domain algebra tyco [class];
       in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
     fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
-      ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
+      ^ (Syntax.string_of_typ (Config.put show_sorts false ctxt) o Type.strip_sorts) ty);
     fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
       (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
       (SOME o Pretty.block) [Pretty.str "supersort: ",