1.1 --- a/doc-src/more_antiquote.ML	Thu Oct 16 23:58:29 2008 +0200
     1.2 +++ b/doc-src/more_antiquote.ML	Fri Oct 17 10:14:12 2008 +0200
     1.3 @@ -29,13 +29,22 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun pr_class ctxt = enclose "\\isa{" "}" o Pretty.output o Pretty.str
     1.8 -  o Sign.extern_class (ProofContext.theory_of ctxt) o Sign.read_class (ProofContext.theory_of ctxt);
     1.9 +val pr_text = enclose "\\isa{" "}" o Pretty.output o Pretty.str;
    1.10 +
    1.11 +fun pr_class ctxt = Sign.read_class (ProofContext.theory_of ctxt)
    1.12 +  #> Sign.extern_class (ProofContext.theory_of ctxt)
    1.13 +  #> pr_text;
    1.14 +
    1.15 +fun pr_type ctxt = Sign.intern_type (ProofContext.theory_of ctxt)
    1.16 +  #> tap (Sign.arity_number (ProofContext.theory_of ctxt))
    1.17 +  #> Sign.extern_type (ProofContext.theory_of ctxt)
    1.18 +  #> pr_text;
    1.19  
    1.20  in
    1.21  
    1.22  val _ = O.add_commands
    1.23 -  [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class))]
    1.24 +  [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class)),
    1.25 +    ("type", ThyOutput.args (Scan.lift Args.name) (K pr_type))]
    1.26  
    1.27  end;
    1.28