diff -r a80d8ec6c998 -r 3dda49e08b9d src/CTT/ex/Synthesis.thy
--- a/src/CTT/ex/Synthesis.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/CTT/ex/Synthesis.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -91,10 +91,10 @@
                 \<times>  (\<Prod>y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
 apply intr
 apply eqintr
-apply (tactic "resolve_tac @{context} [TSimp.split_eqn] 3")
-apply (tactic "SELECT_GOAL (rew_tac @{context} []) 4")
-apply (tactic "resolve_tac @{context} [TSimp.split_eqn] 3")
-apply (tactic "SELECT_GOAL (rew_tac @{context} []) 4")
+apply (tactic "resolve_tac \<^context> [TSimp.split_eqn] 3")
+apply (tactic "SELECT_GOAL (rew_tac \<^context> []) 4")
+apply (tactic "resolve_tac \<^context> [TSimp.split_eqn] 3")
+apply (tactic "SELECT_GOAL (rew_tac \<^context> []) 4")
 apply (rule_tac [3] p = "y" in NC_succ)
   (**  by (resolve_tac @{context} comp_rls 3);  caused excessive branching  **)
 apply rew