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