# HG changeset patch # User wenzelm # Date 1662368975 -7200 # Node ID d45a45eb1aee781cce306f72f285dabcafbac11c # Parent 854e9223767f633ec8d0b0b45e8cc17925f76c91 tuned error message; diff -r 854e9223767f -r d45a45eb1aee src/Pure/config.ML --- 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)