--- a/src/Pure/goal_display.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/goal_display.ML Tue Dec 13 11:51:42 2016 +0100
@@ -19,10 +19,10 @@
structure Goal_Display: GOAL_DISPLAY =
struct
-val goals_limit_raw = Config.declare_option ("goals_limit", @{here});
+val goals_limit_raw = Config.declare_option ("goals_limit", \<^here>);
val goals_limit = Config.int goals_limit_raw;
-val show_main_goal_raw = Config.declare_option ("show_main_goal", @{here});
+val show_main_goal_raw = Config.declare_option ("show_main_goal", \<^here>);
val show_main_goal = Config.bool show_main_goal_raw;