diff -r 2f38fa28e124 -r c2c9bb3c52c6 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Sep 13 13:33:44 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon Sep 13 14:55:21 2010 +0200
@@ -507,6 +507,12 @@
     val ctxt' = Variable.auto_fixes eq ctxt;
   in ProofContext.pretty_term_abbrev ctxt' eq end;
 
+fun pretty_class ctxt =
+  Pretty.str o Type.extern_class (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt;
+
+fun pretty_type ctxt = Pretty.str o Type.extern_type (ProofContext.tsig_of ctxt)
+  o fst o dest_Type o ProofContext.read_type_name_proper ctxt false;
+
 fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
 
 fun pretty_theory ctxt name =
@@ -561,6 +567,8 @@
 val _ = basic_entity "const" (Args.const_proper false) pretty_const;
 val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
 val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
+val _ = basic_entity "class" (Scan.lift Args.name) pretty_class;
+val _ = basic_entity "type" (Scan.lift Args.name) pretty_type;
 val _ = basic_entity "text" (Scan.lift Args.name) pretty_text;
 val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
 val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);