diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Groebner_Basis.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -10,9 +10,9 @@
 
 subsection \<open>Groebner Bases\<close>
 
-lemmas bool_simps = simp_thms(1-34) \<comment> \<open>FIXME move to @{theory HOL.HOL}\<close>
+lemmas bool_simps = simp_thms(1-34) \<comment> \<open>FIXME move to \<^theory>\<open>HOL.HOL\<close>\<close>
 
-lemma nnf_simps: \<comment> \<open>FIXME shadows fact binding in @{theory HOL.HOL}\<close>
+lemma nnf_simps: \<comment> \<open>FIXME shadows fact binding in \<^theory>\<open>HOL.HOL\<close>\<close>
   "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
   "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
   "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"