--- 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);