--- a/src/HOL/Algebra/Sym_Groups.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Algebra/Sym_Groups.thy Sat Jan 05 17:24:33 2019 +0100
@@ -317,7 +317,7 @@
subsection \<open>Unsolvability of Symmetric Groups\<close>
-text \<open>We show that symmetric groups (@{term\<open>sym_group n\<close>}) are unsolvable for @{term\<open>n \<ge> 5\<close>}.\<close>
+text \<open>We show that symmetric groups (\<^term>\<open>sym_group n\<close>) are unsolvable for \<^term>\<open>n \<ge> 5\<close>.\<close>
abbreviation three_cycles :: "nat \<Rightarrow> (nat \<Rightarrow> nat) set"
where "three_cycles n \<equiv>