--- a/src/HOL/Tools/lambda_lifting.ML Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/lambda_lifting.ML Fri Jan 04 23:22:53 2019 +0100
@@ -60,8 +60,8 @@
fun init ctxt = (Termtab.empty, ctxt)
-fun is_quantifier (Const (@{const_name All}, _)) = true
- | is_quantifier (Const (@{const_name Ex}, _)) = true
+fun is_quantifier (Const (\<^const_name>\<open>All\<close>, _)) = true
+ | is_quantifier (Const (\<^const_name>\<open>Ex\<close>, _)) = true
| is_quantifier _ = false
fun lift_lambdas1 is_binder basename =