equal
deleted
inserted
replaced
18 |
18 |
19 (** prepare types/terms: create inference parameters **) |
19 (** prepare types/terms: create inference parameters **) |
20 |
20 |
21 (* constraints *) |
21 (* constraints *) |
22 |
22 |
23 val const_sorts = Config.bool (Config.declare "const_sorts" (K (Config.Bool true))); |
23 val const_sorts = |
|
24 Config.bool (Config.declare ("const_sorts", @{here}) (K (Config.Bool true))); |
24 |
25 |
25 fun const_type ctxt = |
26 fun const_type ctxt = |
26 try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o |
27 try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o |
27 Consts.the_constraint (Proof_Context.consts_of ctxt)); |
28 Consts.the_constraint (Proof_Context.consts_of ctxt)); |
28 |
29 |