1.1 --- a/doc-src/more_antiquote.ML	Sun Mar 14 00:51:58 2010 -0800
     1.2 +++ b/doc-src/more_antiquote.ML	Sun Mar 14 14:10:21 2010 +0100
     1.3 @@ -53,13 +53,13 @@
     1.4  
     1.5  val pr_text = enclose "\\isa{" "}" o Pretty.output o Pretty.str;
     1.6  
     1.7 -fun pr_class ctxt = Sign.read_class (ProofContext.theory_of ctxt)
     1.8 -  #> Sign.extern_class (ProofContext.theory_of ctxt)
     1.9 +fun pr_class ctxt = ProofContext.read_class ctxt
    1.10 +  #> Type.extern_class (ProofContext.tsig_of ctxt)
    1.11    #> pr_text;
    1.12  
    1.13 -fun pr_type ctxt = Sign.intern_type (ProofContext.theory_of ctxt)
    1.14 -  #> tap (Sign.arity_number (ProofContext.theory_of ctxt))
    1.15 -  #> Sign.extern_type (ProofContext.theory_of ctxt)
    1.16 +fun pr_type ctxt = ProofContext.read_type_name_proper ctxt true
    1.17 +  #> (#1 o Term.dest_Type)
    1.18 +  #> Type.extern_type (ProofContext.tsig_of ctxt)
    1.19    #> pr_text;
    1.20  
    1.21  in