--- 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)