diff -r 03a6b1792cd8 -r e96b7be56d44 src/Pure/Isar/subgoal.ML
--- a/src/Pure/Isar/subgoal.ML	Thu Jul 09 22:13:24 2015 +0200
+++ b/src/Pure/Isar/subgoal.ML	Thu Jul 09 22:36:31 2015 +0200
@@ -150,7 +150,8 @@
 fun GEN_FOCUS flags tac ctxt i st =
   if Thm.nprems_of st < i then Seq.empty
   else
-    let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i NONE st;
+    let val (args as {context = ctxt', params, asms, ...}, st') =
+      gen_focus flags (ctxt |> Variable.set_bound_focus true) i NONE st;
     in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
 
 val FOCUS_PARAMS = GEN_FOCUS (false, false);