# HG changeset patch # User wenzelm # Date 1662410829 -7200 # Node ID 319d08115b13a36b35d40f1358c9e9b821fce533 # Parent e39c1da9d904e6a7abd227d534e2fe3daeed9263 clarified options, following e.g. "show_consts"; diff -r e39c1da9d904 -r 319d08115b13 etc/options --- a/etc/options Mon Sep 05 21:59:05 2022 +0200 +++ b/etc/options Mon Sep 05 22:47:09 2022 +0200 @@ -59,6 +59,8 @@ option show_consts : bool = false -- "show constants with types when printing proof state" +option show_goal_inst : bool = false + -- "show goal instantiation (for schematic goals)" option show_main_goal : bool = false -- "show main goal when printing proof state" option goals_limit : int = 10 diff -r e39c1da9d904 -r 319d08115b13 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Mon Sep 05 21:59:05 2022 +0200 +++ b/src/Pure/Isar/proof_display.ML Mon Sep 05 22:47:09 2022 +0200 @@ -248,7 +248,7 @@ (* goal instantiation *) -val show_goal_inst = Attrib.setup_config_bool \<^binding>\show_goal_inst\ (K false); +val show_goal_inst = Attrib.setup_option_bool ("show_goal_inst", \<^here>); fun pretty_goal_inst ctxt propss goal = let