equal
deleted
inserted
replaced
3 imports Main |
3 imports Main |
4 begin |
4 begin |
5 |
5 |
6 ML {* |
6 ML {* |
7 fun pretty_term_type_only ctxt (t, T) = |
7 fun pretty_term_type_only ctxt (t, T) = |
8 (if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then () |
8 (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then () |
9 else error "term_type_only: type mismatch"; |
9 else error "term_type_only: type mismatch"; |
10 Syntax.pretty_typ ctxt T) |
10 Syntax.pretty_typ ctxt T) |
11 |
11 |
12 val _ = Thy_Output.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev) |
12 val _ = Thy_Output.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev) |
13 (fn {source, context = ctxt, ...} => fn arg => |
13 (fn {source, context = ctxt, ...} => fn arg => |