diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/simplifier.ML	Wed Dec 06 18:59:33 2017 +0100
@@ -112,7 +112,7 @@
 val the_simproc = Name_Space.get o get_simprocs;
 
 val _ = Theory.setup
-  (ML_Antiquotation.value @{binding simproc}
+  (ML_Antiquotation.value \<^binding>\<open>simproc\<close>
     (Args.context -- Scan.lift (Parse.position Args.embedded)
       >> (fn (ctxt, name) =>
         "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
@@ -319,13 +319,13 @@
 (* setup attributes *)
 
 val _ = Theory.setup
- (Attrib.setup @{binding simp} (Attrib.add_del simp_add simp_del)
+ (Attrib.setup \<^binding>\<open>simp\<close> (Attrib.add_del simp_add simp_del)
     "declaration of Simplifier rewrite rule" #>
-  Attrib.setup @{binding cong} (Attrib.add_del cong_add cong_del)
+  Attrib.setup \<^binding>\<open>cong\<close> (Attrib.add_del cong_add cong_del)
     "declaration of Simplifier congruence rule" #>
-  Attrib.setup @{binding simproc} simproc_att
+  Attrib.setup \<^binding>\<open>simproc\<close> simproc_att
     "declaration of simplification procedures" #>
-  Attrib.setup @{binding simplified} simplified "simplified rule");
+  Attrib.setup \<^binding>\<open>simplified\<close> simplified "simplified rule");
 
 
 
@@ -368,12 +368,12 @@
 (** setup **)
 
 fun method_setup more_mods =
-  Method.setup @{binding simp}
+  Method.setup \<^binding>\<open>simp\<close>
     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
       HEADGOAL (Method.insert_tac ctxt facts THEN'
         (CHANGED_PROP oo tac) ctxt)))
     "simplification" #>
-  Method.setup @{binding simp_all}
+  Method.setup \<^binding>\<open>simp_all\<close>
     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
       ALLGOALS (Method.insert_tac ctxt facts) THEN
         (CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt))