equal
deleted
inserted
replaced
149 (* constants *) |
149 (* constants *) |
150 |
150 |
151 fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) |
151 fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) |
152 >> (fn (ctxt, (s, pos)) => |
152 >> (fn (ctxt, (s, pos)) => |
153 let |
153 let |
154 val Const (c, _) = Proof_Context.read_const ctxt {proper = true, strict = false} dummyT s; |
154 val Const (c, _) = Proof_Context.read_const ctxt {proper = true, strict = false} s; |
155 val res = check (Proof_Context.consts_of ctxt, c) |
155 val res = check (Proof_Context.consts_of ctxt, c) |
156 handle TYPE (msg, _, _) => error (msg ^ Position.here pos); |
156 handle TYPE (msg, _, _) => error (msg ^ Position.here pos); |
157 in ML_Syntax.print_string res end); |
157 in ML_Syntax.print_string res end); |
158 |
158 |
159 val _ = Theory.setup |
159 val _ = Theory.setup |
174 (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional |
174 (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional |
175 (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
175 (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
176 >> (fn ((ctxt, raw_c), Ts) => |
176 >> (fn ((ctxt, raw_c), Ts) => |
177 let |
177 let |
178 val Const (c, _) = |
178 val Const (c, _) = |
179 Proof_Context.read_const ctxt {proper = true, strict = true} dummyT raw_c; |
179 Proof_Context.read_const ctxt {proper = true, strict = true} raw_c; |
180 val consts = Proof_Context.consts_of ctxt; |
180 val consts = Proof_Context.consts_of ctxt; |
181 val n = length (Consts.typargs consts (c, Consts.type_scheme consts c)); |
181 val n = length (Consts.typargs consts (c, Consts.type_scheme consts c)); |
182 val _ = length Ts <> n andalso |
182 val _ = length Ts <> n andalso |
183 error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^ |
183 error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^ |
184 quote c ^ enclose "(" ")" (commas (replicate n "_"))); |
184 quote c ^ enclose "(" ")" (commas (replicate n "_"))); |