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