--- a/src/Pure/Isar/proof_display.ML Mon Sep 05 21:13:29 2022 +0200
+++ b/src/Pure/Isar/proof_display.ML Mon Sep 05 21:18:40 2022 +0200
@@ -251,7 +251,7 @@
(* goal instantiation *)
-val show_goal_inst = Config.declare_bool ("show_goal_inst", \<^here>) (K false);
+val show_goal_inst = Attrib.setup_config_bool \<^binding>\<open>show_goal_inst\<close> (K false);
fun pretty_goal_inst ctxt propss goal =
let
@@ -328,7 +328,8 @@
Config.declare_bool ("interactive", \<^here>) (K false);
val show_results =
- Config.declare_bool ("show_results", \<^here>) (fn context => Config.get_generic context interactive);
+ Attrib.setup_config_bool \<^binding>\<open>show_results\<close>
+ (fn context => Config.get_generic context interactive);
fun no_print int ctxt = not (Config.get (Config.put interactive int ctxt) show_results);