type antiquotation: allow arbitrary type abbreviations, but fail with user-space exception on bad input
authorhaftmann
Mon, 13 Sep 2010 15:22:40 +0200
changeset 39309 74469faa27ca
parent 39308 c2c9bb3c52c6
child 39310 17ef4415b17c
child 39378 df86b1b4ce10
type antiquotation: allow arbitrary type abbreviations, but fail with user-space exception on bad input
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;