1.1 --- a/src/Pure/Isar/class.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -413,6 +413,8 @@
     1.4  
     1.5  fun print_classes thy =
     1.6    let
     1.7 +    val ctxt = ProofContext.init thy;
     1.8 +
     1.9      val algebra = Sign.classes_of thy;
    1.10      val arities =
    1.11        Symtab.empty
    1.12 @@ -423,13 +425,13 @@
    1.13      fun mk_arity class tyco =
    1.14        let
    1.15          val Ss = Sorts.mg_domain algebra tyco [class];
    1.16 -      in Sign.pretty_arity thy (tyco, Ss, [class]) end;
    1.17 +      in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
    1.18      fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
    1.19 -      ^ setmp show_sorts false (Sign.string_of_typ thy o Type.strip_sorts) ty);
    1.20 +      ^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
    1.21      fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
    1.22        (SOME o Pretty.str) ("class " ^ class ^ ":"),
    1.23        (SOME o Pretty.block) [Pretty.str "supersort: ",
    1.24 -        (Sign.pretty_sort thy o Sign.minimize_sort thy o Sign.super_classes thy) class],
    1.25 +        (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
    1.26        Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class),
    1.27        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
    1.28          o these o Option.map #params o try (AxClass.get_definition thy)) class,