--- 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: ",