author | wenzelm |
Mon, 05 Sep 2022 11:09:35 +0200 | |
changeset 76058 | d45a45eb1aee |
parent 76051 | 854e9223767f |
child 76059 | 7cf72240cdd4 |
--- a/src/Pure/config.ML Sat Sep 03 23:10:38 2022 +0200 +++ b/src/Pure/config.ML Mon Sep 05 11:09:35 2022 +0200 @@ -164,7 +164,7 @@ fun declare_option (name, pos) = let - val typ = Options.default_typ name; + val typ = Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos); val default = if typ = Options.boolT then fn _ => Bool (Options.default_bool name) else if typ = Options.intT then fn _ => Int (Options.default_int name)