src/HOL/Tools/Lifting/lifting_bnf.ML

--- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Fri Jan 04 23:22:53 2019 +0100
@@ -42,7 +42,7 @@
   let
     val argTs = map fastype_of args
   in
-    list_comb (Const (@{const_name Quotient}, argTs ---> HOLogic.boolT), args)
+    list_comb (Const (\<^const_name>\<open>Quotient\<close>, argTs ---> HOLogic.boolT), args)
   end
 
 fun prove_Quotient_map bnf ctxt =
@@ -106,7 +106,7 @@
       lthy |> fold (perhaps o try o (snd oo Local_Theory.notes)) notess
     end
 
-val lifting_plugin = Plugin_Name.declare_setup @{binding lifting}
+val lifting_plugin = Plugin_Name.declare_setup \<^binding>\<open>lifting\<close>
 
 val _ =
   Theory.setup