src/HOL/Tools/set_comprehension_pointfree.ML
changeset 60696 8304fb4fb823
parent 59621 291934bac95e
child 60781 2da59cdf531c
     1.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Jul 08 19:28:43 2015 +0200
     1.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Jul 08 21:33:00 2015 +0200
     1.3 @@ -441,9 +441,8 @@
     1.4        THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms exE}
     1.5        THEN' eresolve_tac ctxt @{thms conjE}
     1.6        THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms Pair_inject}
     1.7 -      THEN' Subgoal.FOCUS (fn {prems, ...} =>
     1.8 -        (* FIXME inner context!? *)
     1.9 -        simp_tac (put_simpset HOL_basic_ss ctxt addsimps (filter is_eq prems)) 1) ctxt
    1.10 +      THEN' Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
    1.11 +        simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (filter is_eq prems)) 1) ctxt
    1.12        THEN' TRY o assume_tac ctxt
    1.13    in
    1.14      case try mk_term (Thm.term_of ct) of