# 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)