equal
deleted
inserted
replaced
176 (Args.context -- Scan.lift Args.name_source -- Scan.optional |
176 (Args.context -- Scan.lift Args.name_source -- Scan.optional |
177 (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
177 (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
178 >> (fn ((ctxt, raw_c), Ts) => |
178 >> (fn ((ctxt, raw_c), Ts) => |
179 let |
179 let |
180 val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c; |
180 val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c; |
181 val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts)); |
181 val consts = Proof_Context.consts_of ctxt; |
|
182 val n = length (Consts.typargs consts (c, Consts.type_scheme consts c)); |
|
183 val _ = length Ts <> n andalso |
|
184 error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^ |
|
185 quote c ^ enclose "(" ")" (commas (replicate n "_"))); |
|
186 val const = Const (c, Consts.instance consts (c, Ts)); |
182 in ML_Syntax.atomic (ML_Syntax.print_term const) end)))); |
187 in ML_Syntax.atomic (ML_Syntax.print_term const) end)))); |
183 |
188 |
184 |
189 |
185 (* outer syntax *) |
190 (* outer syntax *) |
186 |
191 |