src/Pure/goal_display.ML
changeset 51960 61ac1efe02c3
parent 51959 18d758e38d85
child 52043 286629271d65
     1.1 --- a/src/Pure/goal_display.ML	Mon May 13 13:01:10 2013 +0200
     1.2 +++ b/src/Pure/goal_display.ML	Mon May 13 13:23:13 2013 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  
     1.5  signature GOAL_DISPLAY =
     1.6  sig
     1.7 -  val goals_limit_default: int Unsynchronized.ref
     1.8    val goals_limit_raw: Config.raw
     1.9    val goals_limit: int Config.T
    1.10    val show_main_goal_default: bool Unsynchronized.ref
    1.11 @@ -26,8 +25,7 @@
    1.12  structure Goal_Display: GOAL_DISPLAY =
    1.13  struct
    1.14  
    1.15 -val goals_limit_default = Unsynchronized.ref 10;
    1.16 -val goals_limit_raw = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
    1.17 +val goals_limit_raw = Config.declare_option "goals_limit";
    1.18  val goals_limit = Config.int goals_limit_raw;
    1.19  
    1.20  val show_main_goal_default = Unsynchronized.ref false;