src/HOL/Tools/simpdata.ML
changeset 58957 c9e744ea8a38
parent 58839 ccda99401bc8
child 58963 26bf09b95dda
     1.1 --- a/src/HOL/Tools/simpdata.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/HOL/Tools/simpdata.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -120,9 +120,9 @@
     1.4        reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
     1.5      fun sol_tac i =
     1.6        FIRST [resolve_tac sol_thms i, assume_tac i , eresolve_tac @{thms FalseE} i] ORELSE
     1.7 -      (match_tac intros THEN_ALL_NEW sol_tac) i
     1.8 +      (match_tac ctxt intros THEN_ALL_NEW sol_tac) i
     1.9    in
    1.10 -    (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' sol_tac
    1.11 +    (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN' sol_tac
    1.12    end;
    1.13  
    1.14  val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
    1.15 @@ -130,9 +130,9 @@
    1.16  
    1.17  (*No premature instantiation of variables during simplification*)
    1.18  fun safe_solver_tac ctxt =
    1.19 -  (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
    1.20 -  FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt),
    1.21 -    eq_assume_tac, ematch_tac @{thms FalseE}];
    1.22 +  (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN'
    1.23 +  FIRST' [match_tac ctxt (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt),
    1.24 +    eq_assume_tac, ematch_tac ctxt @{thms FalseE}];
    1.25  
    1.26  val safe_solver = mk_solver "HOL safe" safe_solver_tac;
    1.27