src/Pure/goal_display.ML
changeset 52043 286629271d65
parent 51960 61ac1efe02c3
child 52185 1b481b490454
     1.1 --- a/src/Pure/goal_display.ML	Thu May 16 21:09:58 2013 +0200
     1.2 +++ b/src/Pure/goal_display.ML	Thu May 16 21:48:01 2013 +0200
     1.3 @@ -9,10 +9,8 @@
     1.4  sig
     1.5    val goals_limit_raw: Config.raw
     1.6    val goals_limit: int Config.T
     1.7 -  val show_main_goal_default: bool Unsynchronized.ref
     1.8    val show_main_goal_raw: Config.raw
     1.9    val show_main_goal: bool Config.T
    1.10 -  val show_consts_default: bool Unsynchronized.ref
    1.11    val show_consts_raw: Config.raw
    1.12    val show_consts: bool Config.T
    1.13    val pretty_flexpair: Proof.context -> term * term -> Pretty.T
    1.14 @@ -28,13 +26,10 @@
    1.15  val goals_limit_raw = Config.declare_option "goals_limit";
    1.16  val goals_limit = Config.int goals_limit_raw;
    1.17  
    1.18 -val show_main_goal_default = Unsynchronized.ref false;
    1.19 -val show_main_goal_raw =
    1.20 -  Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
    1.21 +val show_main_goal_raw = Config.declare_option "show_main_goal";
    1.22  val show_main_goal = Config.bool show_main_goal_raw;
    1.23  
    1.24 -val show_consts_default = Unsynchronized.ref false;
    1.25 -val show_consts_raw = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
    1.26 +val show_consts_raw = Config.declare_option "show_consts";
    1.27  val show_consts = Config.bool show_consts_raw;
    1.28  
    1.29  fun pretty_flexpair ctxt (t, u) = Pretty.block