diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Tools/SMT/smtlib_proof.ML
--- a/src/HOL/Tools/SMT/smtlib_proof.ML	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Tools/SMT/smtlib_proof.ML	Sat Jan 05 17:24:33 2019 +0100
@@ -140,8 +140,8 @@
 fun mk_less t1 t2 = mk_binary_pred \<^const_name>\<open>ord_class.less\<close> \<^sort>\<open>linorder\<close> t1 t2
 fun mk_less_eq t1 t2 = mk_binary_pred \<^const_name>\<open>ord_class.less_eq\<close> \<^sort>\<open>linorder\<close> t1 t2
 
-fun core_term_parser (SMTLIB.Sym "true", _) = SOME @{const HOL.True}
-  | core_term_parser (SMTLIB.Sym "false", _) = SOME @{const HOL.False}
+fun core_term_parser (SMTLIB.Sym "true", _) = SOME \<^const>\<open>HOL.True\<close>
+  | core_term_parser (SMTLIB.Sym "false", _) = SOME \<^const>\<open>HOL.False\<close>
   | core_term_parser (SMTLIB.Sym "not", [t]) = SOME (HOLogic.mk_not t)
   | core_term_parser (SMTLIB.Sym "and", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_conj) t ts)
   | core_term_parser (SMTLIB.Sym "or", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_disj) t ts)