diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/more_thm.ML	Tue Dec 13 11:51:42 2016 +0100
@@ -654,13 +654,13 @@
 
 (* options *)
 
-val show_consts_raw = Config.declare_option ("show_consts", @{here});
+val show_consts_raw = Config.declare_option ("show_consts", \<^here>);
 val show_consts = Config.bool show_consts_raw;
 
-val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false);
+val show_hyps_raw = Config.declare ("show_hyps", \<^here>) (fn _ => Config.Bool false);
 val show_hyps = Config.bool show_hyps_raw;
 
-val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false);
+val show_tags_raw = Config.declare ("show_tags", \<^here>) (fn _ => Config.Bool false);
 val show_tags = Config.bool show_tags_raw;