# HG changeset patch # User wenzelm # Date 1662405520 -7200 # Node ID 6dc5968b9a860ddc662de53977f2c8a5b4a02b58 # Parent 28ddebb43d93ff206bd019ecb156184502d6dd3f clarified modules; diff -r 28ddebb43d93 -r 6dc5968b9a86 src/Pure/Isar/attrib.ML --- 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 #> diff -r 28ddebb43d93 -r 6dc5968b9a86 src/Pure/Isar/proof_display.ML --- 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>\show_goal_inst\ (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>\show_results\ + (fn context => Config.get_generic context interactive); fun no_print int ctxt = not (Config.get (Config.put interactive int ctxt) show_results); diff -r 28ddebb43d93 -r 6dc5968b9a86 src/Pure/ROOT.ML --- 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";