60 ML_Antiquotation.inline @{binding typ} (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> |
60 ML_Antiquotation.inline @{binding typ} (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> |
61 ML_Antiquotation.inline @{binding term} (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> |
61 ML_Antiquotation.inline @{binding term} (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> |
62 ML_Antiquotation.inline @{binding prop} (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> |
62 ML_Antiquotation.inline @{binding prop} (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> |
63 |
63 |
64 ML_Antiquotation.value @{binding ctyp} (Args.typ >> (fn T => |
64 ML_Antiquotation.value @{binding ctyp} (Args.typ >> (fn T => |
65 "Proof_Context.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #> |
65 "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #> |
66 |
66 |
67 ML_Antiquotation.value @{binding cterm} (Args.term >> (fn t => |
67 ML_Antiquotation.value @{binding cterm} (Args.term >> (fn t => |
68 "Proof_Context.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> |
68 "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> |
69 |
69 |
70 ML_Antiquotation.value @{binding cprop} (Args.prop >> (fn t => |
70 ML_Antiquotation.value @{binding cprop} (Args.prop >> (fn t => |
71 "Proof_Context.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> |
71 "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> |
72 |
72 |
73 ML_Antiquotation.value @{binding cpat} |
73 ML_Antiquotation.value @{binding cpat} |
74 (Args.context -- |
74 (Args.context -- |
75 Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t => |
75 Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t => |
76 "Proof_Context.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); |
76 "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); |
77 |
77 |
78 |
78 |
79 (* type classes *) |
79 (* type classes *) |
80 |
80 |
81 fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) => |
81 fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) => |