type antiquotation: allow arbitrary type abbreviations, but fail with user-space exception on bad input
--- a/src/Pure/Thy/thy_output.ML Mon Sep 13 14:55:21 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Mon Sep 13 15:22:40 2010 +0200
@@ -510,8 +510,11 @@
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_type ctxt s =
+ let
+ val tsig = ProofContext.tsig_of ctxt;
+ val _ = ProofContext.read_type_name ctxt false s;
+ in (Pretty.str o Type.extern_type tsig o Type.intern_type tsig) s end;
fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;