diff -r a80d8ec6c998 -r 3dda49e08b9d src/CTT/ex/Equality.thy
--- a/src/CTT/ex/Equality.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/CTT/ex/Equality.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -47,7 +47,7 @@
 lemma "p : Sum(A,B) \<Longrightarrow> <split(p,\<lambda>x y. x), split(p,\<lambda>x y. y)> = p : Sum(A,B)"
 apply (rule EqE)
 apply (rule elim_rls, assumption)
-apply (tactic \<open>DEPTH_SOLVE_1 (rew_tac @{context} [])\<close>) (*!!!!!!!*)
+apply (tactic \<open>DEPTH_SOLVE_1 (rew_tac \<^context> [])\<close>) (*!!!!!!!*)
 done
 
 lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>u. split(u, \<lambda>v w.<w,v>)) ` <a,b> = <b,a> : \<Sum>x:B. A"