clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees;
tuned;

--- a/NEWS	Fri Sep 24 15:56:29 2010 +0200
+++ b/NEWS	Fri Sep 24 16:17:59 2010 +0200
@@ -68,7 +68,7 @@
 * Discontinued ancient 'constdefs' command.  INCOMPATIBILITY, use
 'definition' instead.
 
-* Document antiquotations 'class' and 'type' for printing classes
+* Document antiquotations @{class} and @{type} for printing classes
 and type constructors.
 
 

--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Sep 24 15:56:29 2010 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Sep 24 16:17:59 2010 +0200
@@ -250,8 +250,8 @@
 
   \item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
 
-  \item @{text "@{type \<kappa>}"} prints a type constructor
-    (logical or abbreviation) @{text "\<kappa>"}.
+  \item @{text "@{type \<kappa>}"} prints a (logical or syntactic) type
+    constructor @{text "\<kappa>"}.
 
   \item @{text "@{class c}"} prints a class @{text c}.
 

--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Sep 24 15:56:29 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Sep 24 16:17:59 2010 +0200
@@ -266,8 +266,8 @@
 
   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}} prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
 
-  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}type\ {\isasymkappa}{\isacharbraceright}{\isachardoublequote}} prints a type constructor
-    (logical or abbreviation) \isa{{\isachardoublequote}{\isasymkappa}{\isachardoublequote}}.
+  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}type\ {\isasymkappa}{\isacharbraceright}{\isachardoublequote}} prints a (logical or syntactic) type
+    constructor \isa{{\isachardoublequote}{\isasymkappa}{\isachardoublequote}}.
 
   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}class\ c{\isacharbraceright}{\isachardoublequote}} prints a class \isa{c}.
 

--- a/src/Pure/Thy/thy_output.ML	Fri Sep 24 15:56:29 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Sep 24 16:17:59 2010 +0200
@@ -511,10 +511,8 @@
   Pretty.str o Type.extern_class (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt;
 
 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;
+  let val Type (name, _) = ProofContext.read_type_name_proper ctxt false s
+  in Pretty.str (Type.extern_type (ProofContext.tsig_of ctxt) name) end;
 
 fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;