diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Auth/Recur.thy Mon Nov 10 21:49:48 2014 +0100 @@ -163,7 +163,7 @@ [THEN respond.Cons, THEN respond.Cons]], THEN recur.RA4, THEN recur.RA4]) apply basic_possibility -apply (tactic "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1)") +apply (tactic "DEPTH_SOLVE (swap_res_tac @{context} [refl, conjI, disjCI] 1)") done