--- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -199,7 +199,7 @@
 apply (drule spec, erule impE)
 apply  (erule BufAC_Asm_antiton [THEN antitonPD])
 apply  (erule is_ub_thelub)
-apply (tactic "smp_tac @{context} 3 1")
+apply (tactic "smp_tac \<^context> 3 1")
 apply (drule is_ub_thelub)
 apply (drule (1) mp)
 apply (drule (1) mp)