src/HOL/Tools/set_comprehension_pointfree.ML

       THEN' REPEAT_DETERM o resolve_tac ctxt @{thms exI}
       THEN' resolve_tac ctxt @{thms conjI} THEN' resolve_tac ctxt @{thms refl} THEN' assume_tac ctxt
       THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms exE}
       THEN' eresolve_tac ctxt @{thms conjE}
       THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms Pair_inject}
-      THEN' Subgoal.FOCUS (fn {prems, ...} =>
-        (* FIXME inner context!? *)
-        simp_tac (put_simpset HOL_basic_ss ctxt addsimps (filter is_eq prems)) 1) ctxt
+      THEN' Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
+        simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (filter is_eq prems)) 1) ctxt
       THEN' TRY o assume_tac ctxt
   in
     case try mk_term (Thm.term_of ct) of
       NONE => Thm.reflexive ct
     | SOME t' =>