src/Pure/Isar/class.ML
changeset 39134 917b4b6ba3d2
parent 39133 70d3915c92f0
child 39378 df86b1b4ce10
     1.1 --- a/src/Pure/Isar/class.ML	Sun Sep 05 19:47:40 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sun Sep 05 21:41:24 2010 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4          val Ss = Sorts.mg_domain algebra tyco [class];
     1.5        in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
     1.6      fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
     1.7 -      ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
     1.8 +      ^ (Syntax.string_of_typ (Config.put show_sorts false ctxt) o Type.strip_sorts) ty);
     1.9      fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
    1.10        (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
    1.11        (SOME o Pretty.block) [Pretty.str "supersort: ",