src/Pure/goal_display.ML
changeset 56438 7f6b2634d853
parent 52284 b12f2cef3ee5
child 56493 1f660d858a75
     1.1 --- a/src/Pure/goal_display.ML	Sun Apr 06 15:51:02 2014 +0200
     1.2 +++ b/src/Pure/goal_display.ML	Sun Apr 06 16:36:28 2014 +0200
     1.3 @@ -23,13 +23,13 @@
     1.4  structure Goal_Display: GOAL_DISPLAY =
     1.5  struct
     1.6  
     1.7 -val goals_limit_raw = Config.declare_option "goals_limit";
     1.8 +val goals_limit_raw = Config.declare_option ("goals_limit", @{here});
     1.9  val goals_limit = Config.int goals_limit_raw;
    1.10  
    1.11 -val show_main_goal_raw = Config.declare_option "show_main_goal";
    1.12 +val show_main_goal_raw = Config.declare_option ("show_main_goal", @{here});
    1.13  val show_main_goal = Config.bool show_main_goal_raw;
    1.14  
    1.15 -val show_consts_raw = Config.declare_option "show_consts";
    1.16 +val show_consts_raw = Config.declare_option ("show_consts", @{here});
    1.17  val show_consts = Config.bool show_consts_raw;
    1.18  
    1.19  fun pretty_flexpair ctxt (t, u) = Pretty.block