# HG changeset patch
# User haftmann
# Date 1284384160 -7200
# Node ID 74469faa27cac685908f9e65475dc239e2e32e57
# Parent  c2c9bb3c52c6edfef6df2ffd47fde7901696a9db
type antiquotation: allow arbitrary type abbreviations, but fail with user-space exception on bad input

diff -r c2c9bb3c52c6 -r 74469faa27ca src/Pure/Thy/thy_output.ML
--- 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;