# HG changeset patch
# User wenzelm
# Date 1268572221 -3600
# Node ID 9d8cd1ca8c6144610ca6fb8ef2395a0c1edc4bdc
# Parent  cdaf99fddd174ae34548afc749ebfe43bf0999a5
localized @{class} and @{type};

diff -r cdaf99fddd17 -r 9d8cd1ca8c61 doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Sun Mar 14 00:51:58 2010 -0800
+++ b/doc-src/more_antiquote.ML	Sun Mar 14 14:10:21 2010 +0100
@@ -53,13 +53,13 @@
 
 val pr_text = enclose "\\isa{" "}" o Pretty.output o Pretty.str;
 
-fun pr_class ctxt = Sign.read_class (ProofContext.theory_of ctxt)
-  #> Sign.extern_class (ProofContext.theory_of ctxt)
+fun pr_class ctxt = ProofContext.read_class ctxt
+  #> Type.extern_class (ProofContext.tsig_of ctxt)
   #> pr_text;
 
-fun pr_type ctxt = Sign.intern_type (ProofContext.theory_of ctxt)
-  #> tap (Sign.arity_number (ProofContext.theory_of ctxt))
-  #> Sign.extern_type (ProofContext.theory_of ctxt)
+fun pr_type ctxt = ProofContext.read_type_name_proper ctxt true
+  #> (#1 o Term.dest_Type)
+  #> Type.extern_type (ProofContext.tsig_of ctxt)
   #> pr_text;
 
 in