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