equal
deleted
inserted
replaced
51 |
51 |
52 local |
52 local |
53 |
53 |
54 val pr_text = enclose "\\isa{" "}" o Pretty.output o Pretty.str; |
54 val pr_text = enclose "\\isa{" "}" o Pretty.output o Pretty.str; |
55 |
55 |
56 fun pr_class ctxt = Sign.read_class (ProofContext.theory_of ctxt) |
56 fun pr_class ctxt = ProofContext.read_class ctxt |
57 #> Sign.extern_class (ProofContext.theory_of ctxt) |
57 #> Type.extern_class (ProofContext.tsig_of ctxt) |
58 #> pr_text; |
58 #> pr_text; |
59 |
59 |
60 fun pr_type ctxt = Sign.intern_type (ProofContext.theory_of ctxt) |
60 fun pr_type ctxt = ProofContext.read_type_name_proper ctxt true |
61 #> tap (Sign.arity_number (ProofContext.theory_of ctxt)) |
61 #> (#1 o Term.dest_Type) |
62 #> Sign.extern_type (ProofContext.theory_of ctxt) |
62 #> Type.extern_type (ProofContext.tsig_of ctxt) |
63 #> pr_text; |
63 #> pr_text; |
64 |
64 |
65 in |
65 in |
66 |
66 |
67 val _ = ThyOutput.antiquotation "class" (Scan.lift Args.name) (pr_class o #context); |
67 val _ = ThyOutput.antiquotation "class" (Scan.lift Args.name) (pr_class o #context); |