| changeset 69575 | f77cc54f6d47 |
| parent 64556 | 851ae0e7b09c |
| child 79411 | 700d4f16b5f2 |
--- a/src/Pure/type_infer_context.ML Thu Jan 03 12:34:26 2019 +0100 +++ b/src/Pure/type_infer_context.ML Thu Jan 03 14:12:44 2019 +0100 @@ -20,8 +20,7 @@ (* constraints *) -val const_sorts = - Config.bool (Config.declare ("const_sorts", \<^here>) (K (Config.Bool true))); +val const_sorts = Config.declare_bool ("const_sorts", \<^here>) (K true); fun const_type ctxt = try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o