clarified modules;

--- a/src/Pure/Isar/attrib.ML	Mon Sep 05 21:13:29 2022 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Sep 05 21:18:40 2022 +0200
@@ -601,8 +601,6 @@
   register_config_bool Thm.show_consts #>
   register_config_bool Thm.show_hyps #>
   register_config_bool Thm.show_tags #>
-  register_config_bool Proof_Display.show_goal_inst #>
-  register_config_bool Proof_Display.show_results #>
   register_config_bool Pattern.unify_trace_failure #>
   register_config_int Unify.trace_bound #>
   register_config_int Unify.search_bound #>

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

--- a/src/Pure/ROOT.ML	Mon Sep 05 21:13:29 2022 +0200
+++ b/src/Pure/ROOT.ML	Mon Sep 05 21:18:40 2022 +0200
@@ -250,8 +250,8 @@
 (*basic proof engine*)
 ML_file "par_tactical.ML";
 ML_file "context_tactic.ML";
+ML_file "Isar/attrib.ML";
 ML_file "Isar/proof_display.ML";
-ML_file "Isar/attrib.ML";
 ML_file "Isar/context_rules.ML";
 ML_file "Isar/method.ML";
 ML_file "Isar/proof.ML";