diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Jan 05 17:24:33 2019 +0100
@@ -222,10 +222,10 @@
       end
   end
 
-fun s_not (@{const Not} $ t) = t
+fun s_not (\<^const>\<open>Not\<close> $ t) = t
   | s_not t = HOLogic.mk_not t
-fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t
-  | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
+fun simp_not_not (\<^const>\<open>Trueprop\<close> $ t) = \<^const>\<open>Trueprop\<close> $ simp_not_not t
+  | simp_not_not (\<^const>\<open>Not\<close> $ t) = s_not (simp_not_not t)
   | simp_not_not t = t
 
 val normalize_literal = simp_not_not o Envir.eta_contract