--- 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