diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Tools/SMT/verit_proof.ML
--- a/src/HOL/Tools/SMT/verit_proof.ML	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Tools/SMT/verit_proof.ML	Sat Jan 05 17:24:33 2019 +0100
@@ -383,7 +383,7 @@
         fun inline_assumption assumption assumption_id
             (VeriT_Node {id, rule, prems, proof_ctxt, concl, bounds}) =
           mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt
-            (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
+            (\<^const>\<open>Pure.imp\<close> $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
         fun find_input_steps_and_inline [] = []
           | find_input_steps_and_inline
               (VeriT_Node {id = id', rule, prems, concl, bounds, ...} :: steps) =