src/Pure/tactic.ML
changeset 58957 c9e744ea8a38
parent 58956 a816aa3ff391
child 58963 26bf09b95dda
     1.1 --- a/src/Pure/tactic.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/Pure/tactic.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -24,10 +24,10 @@
     1.4    val ftac: thm -> int -> tactic
     1.5    val ares_tac: thm list -> int -> tactic
     1.6    val solve_tac: thm list -> int -> tactic
     1.7 -  val bimatch_tac: (bool * thm) list -> int -> tactic
     1.8 -  val match_tac: thm list -> int -> tactic
     1.9 -  val ematch_tac: thm list -> int -> tactic
    1.10 -  val dmatch_tac: thm list -> int -> tactic
    1.11 +  val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic
    1.12 +  val match_tac: Proof.context -> thm list -> int -> tactic
    1.13 +  val ematch_tac: Proof.context -> thm list -> int -> tactic
    1.14 +  val dmatch_tac: Proof.context -> thm list -> int -> tactic
    1.15    val flexflex_tac: Proof.context -> tactic
    1.16    val distinct_subgoal_tac: int -> tactic
    1.17    val distinct_subgoals_tac: tactic
    1.18 @@ -146,10 +146,10 @@
    1.19  fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
    1.20  
    1.21  (*Matching tactics -- as above, but forbid updating of state*)
    1.22 -fun bimatch_tac brules i = PRIMSEQ (Thm.biresolution NONE true brules i);
    1.23 -fun match_tac rules  = bimatch_tac (map (pair false) rules);
    1.24 -fun ematch_tac rules = bimatch_tac (map (pair true) rules);
    1.25 -fun dmatch_tac rls   = ematch_tac (map make_elim rls);
    1.26 +fun bimatch_tac ctxt brules i = PRIMSEQ (Thm.biresolution (SOME ctxt) true brules i);
    1.27 +fun match_tac ctxt rules = bimatch_tac ctxt (map (pair false) rules);
    1.28 +fun ematch_tac ctxt rules = bimatch_tac ctxt (map (pair true) rules);
    1.29 +fun dmatch_tac ctxt rls = ematch_tac ctxt (map make_elim rls);
    1.30  
    1.31  (*Smash all flex-flex disagreement pairs in the proof state.*)
    1.32  fun flexflex_tac ctxt = PRIMSEQ (Thm.flexflex_rule (SOME ctxt));